编程理论实践：2015-9-19版

需积分: 12 92 浏览量更新于2024-07-21 收藏 1.29MB PDF 举报

身份认证购VIP最低享 7 折!

领优惠券(最高得80元）

"《实用编程理论 2015-9-19 版》是 Eric C. R. Hehner 所著的一本关于编程理论的书籍，它提出了一种比传统编程理论更为简洁且通用的理论。在这个理论中，规格说明仅仅是一个布尔表达式，而细化则是普通的蕴含关系。此理论适用于终止和非终止计算，顺序和并行计算，独立和交互式计算，并且还包含了时间限制，可用于算法分类和实时应用。书中涵盖了二进制理论、数论、字符理论、基本数据结构（如 bunch 理论、集合理论、字符串理论和列表理论）以及函数理论等内容。" 在编程理论中，该书提出了一个简化版的理论框架。传统的编程理论，如Hoare逻辑，通常涉及预条件和后条件的配对来指定程序的行为，而Dijkstra的方法则利用最弱前条件谓词变换器。Hehner的理论则将规格说明简化为布尔表达式，这使得理解和应用变得更加直观。细化的概念，即一个更具体的程序或数据结构可以实现一个更抽象的表示，被解释为普通的蕴含关系，这意味着如果一个更复杂的系统满足了简单系统的所有条件，那么它就实现了这个简单系统。书中详细介绍了基础理论，包括二进制理论，其定义了基本的逻辑和证明规则；数论，探讨了数值计算的基础；字符理论，处理字符操作；以及基本数据结构，如bunch（一种数据组织形式），可选的集合理论，字符串理论和列表理论，这些都为理解数据存储和操作提供了基础。列表理论还扩展到了多维结构，这在处理复杂数据时非常重要。此外，函数理论是另一个关键部分，讨论了函数的表示和缩写，以及它们如何被用来构建和操作程序。这部分可能包含函数定义，简化的函数表示，以及如何通过函数来实现其他复杂功能。《实用编程理论》提供了一个全面而易懂的框架，不仅适用于常规的计算模型，还考虑了并发和实时计算的情景，强调了时间和效率的重要性。这本书对于程序员、软件工程师和计算机科学学生来说，是一份深入了解编程本质和理论的重要资源。

资源详情

资源推荐

1.0.2 Monotonicity and Antimonotonicity

A proof can be a continuing equation, as we have seen; it can also be a continuing implication, or a

continuing mixture of equations and implications. As an example, here is a proof of the first Law

of Conflation, which says

(a ⇒ b) ∧ (c ⇒ d)

⇒ a ∧ c ⇒ b ∧ d

The proof goes this way: starting with the right side,

a ∧ c ⇒ b ∧ d distribute ⇒ over second ∧

= (a ∧ c ⇒ b) ∧ (a ∧ c ⇒ d) antidistribution twice

= ((a⇒b) ∨ (c⇒b)) ∧ ((a⇒d) ∨ (c⇒d)) distribute ∧ over ∨ twice

= (a⇒b)∧(a⇒d) ∨ (a⇒b)∧(c⇒d) ∨ (c⇒b)∧(a⇒d) ∨ (c⇒b)∧(c⇒d) generalization

⇐ (a⇒b) ∧ (c⇒d)

From the mutual transitivity of

= and ⇐ , we have proven

a ∧ c ⇒ b ∧ d

⇐ (a⇒b) ∧ (c⇒d)

which can easily be rearranged to give the desired theorem.

The implication operator is reflexive a⇒a , antisymmetric (a⇒b) ∧ (b⇒a) = (a=b) , and

transitive (a⇒b) ∧ (b⇒c) ⇒ (a⇒c) . It is therefore an ordering (just like ≤ for numbers). We

pronounce a⇒b either as “ a implies b ”, or, to emphasize the ordering, as “ a is

stronger than

or equal to b ”. Likewise a⇐b is pronounced either as “ a is implied by b ”, or as “ a is

weaker than or equal to b ”. The words “stronger” and “weaker” may have come from a

philosophical origin; we ignore any meaning they may have other than the binary order, in which

⊥⊥

is stronger than T .

The Monotonic Law a⇒b

⇒ c∧a ⇒ c∧b can be read (a little carelessly) as follows: if a is

weakened to b , then c∧a is weakened to c∧b . (To be more careful, we should say “weakened or

equal”.) If we weaken a , then we weaken c∧a . Or, the other way round, if we strengthen b ,

then we strengthen c∧b . Whatever happens to a conjunct (weaken or strengthen), the same

happens to the conjunction. We say that conjunction is

monotonic in its conjuncts.

The Antimonotonic Law a⇒b

⇒ (b⇒c) ⇒ (a⇒c) says that whatever happens to an antecedent

(weaken or strengthen), the opposite happens to the implication. We say that implication is

antimonotonic in its antecedent.

Here are the monotonic and antimonotonic properties of binary expressions.

¬a is antimonotonic in a

a∧b is monotonic in a and monotonic in b

a∨b is monotonic in a and monotonic in b

a⇒b is antimonotonic in a and monotonic in b

a⇐b is monotonic in a and antimonotonic in b

if a then b else c fi is monotonic in b and monotonic in c

These properties are useful in proofs. For example, in Exercise 2(k), to prove ¬(a ∧ ¬(a∨b)) , we

can employ the Law of Generalization a ⇒ a∨b to strengthen a∨b to a . That weakens ¬(a∨b)

and that weakens a ∧ ¬(a∨b) and that strengthens ¬

(a ∧ ¬(a∨b)) .

¬(a ∧ ¬(a∨b)) use the Law of Generalization

⇐ ¬(a ∧ ¬a) now use the Law of Noncontradiction

= T

We thus prove that ¬(a ∧ ¬(a∨b))

⇐ T , and by an identity law, that is the same as proving

¬(a ∧ ¬(a∨b)) . In other words, ¬(a ∧ ¬(a∨b)) is weaker than or equal to T , and since there is

9 1 Basic Theories

nothing weaker than T , it is equal to T . When we drive toward T , the left edge of the proof can

be any mixture of

= and ⇐ signs.

Similarly we can drive toward ⊥⊥

⊥⊥

, and then the left edge of the proof can be any mixture of

= and

⇒ signs. For example,

a ∧ ¬(a∨b) use the Law of Generalization

⇒ a ∧ ¬a now use the Law of Noncontradiction

= ⊥⊥

⊥⊥

This is called “proof by contradiction”. It proves a ∧ ¬(a∨b)

⇒ ⊥⊥

⊥⊥

, which is the same as

proving ¬(a ∧ ¬(a∨b)) . Any proof by contradiction can be converted to a proof by simplification

to T at the cost of one ¬ sign per line.

End of Monotonicity and Antimonotonicity

1.0.3 Context

A proof, or part of a proof, can make use of local assumptions. A proof may have the format

assumption

⇒ ( expression0

= expression1

= expression2

= expression3 )

for example. The step expression0 = expression1 can make use of the assumption just as

though it were an axiom. So can the step expression1 = expression2 , and so on. Within the

parentheses we have a proof; it can be any kind of proof including one that makes further local

assumptions. We thus can have proofs within proofs, indenting appropriately. If the subproof is

proving expression0 = expression3 , then the whole proof is proving

assumption ⇒ (expression0 = expression3)

If the subproof is proving expression0 , then the whole proof is proving

assumption ⇒ expression0

If the subproof is proving ⊥⊥

⊥⊥

, then the whole proof is proving

assumption ⇒ ⊥⊥

⊥⊥

which is equal to ¬assumption . Once again, this is “proof by contradiction”.

We can also use if then else fi as a proof, or part of a proof, in a similar manner. The format is

if possibility

then first subproof

assuming possibility

as a local axiom

else second subproof

assuming ¬possibility

as a local axiom fi

If the first subproof proves something and the second proves anotherthing , the whole proof

proves

if possibility then something else anotherthing fi

If both subproofs prove the same thing, then by the Case Idempotent Law, so does the whole proof,

and that is its most frequent use.

Consider a step in a proof that looks like this:

expression0 ∧ expression1

= expression0 ∧ expression2

1 Basic Theories 10

When we are changing expression1 into expression2 , we can assume expression0 as a local

axiom just for this step. If expression0 really is a theorem, then we have done no harm by

assuming it as a local axiom. If, however, expression0 is an antitheorem, then both

expression0 ∧ expression1 and expression0 ∧ expression2 are antitheorems no matter what

expression1 and expression2 are, so again we have done nothing wrong. Symmetrically, when

proving

expression0 ∧ expression1

= expression2 ∧ expression1

we can assume expression1 as a local axiom. However, when proving

expression0 ∧ expression1

= expression2 ∧ expression3

we cannot assume expression0 to prove expression1=expression3 and in the same step assume

expression1 to prove expression0=expression2 . For example, starting from a ∧ a , we can

assume the first a and so change the second one to T ,

a ∧ a assume first a to simplify second a

= a ∧ T

or we can assume the second a and so change the first one to T ,

a ∧ a assume second a to simplify first a

= T ∧ a

but we cannot assume both of them at the same time.

a ∧ a this step is wrong

= T ∧ T

In this paragraph, the equal signs could have been implications in either direction.

Here is a list of context rules for proof.

In expression0 ∧ expression1 , when changing expression0 , we can assume expression1 .

In expression0 ∧ expression1 , when changing expression1 , we can assume expression0 .

In expression0 ∨ expression1 , when changing expression0 , we can assume ¬expression1 .

In expression0 ∨ expression1 , when changing expression1 , we can assume ¬expression0 .

In expression0 ⇒ expression1 , when changing expression0 , we can assume ¬expression1 .

In expression0 ⇒ expression1 , when changing expression1 , we can assume expression0 .

In expression0 ⇐ expression1 , when changing expression0 , we can assume expression1 .

In expression0 ⇐ expression1 , when changing expression1 , we can assume ¬expression0 .

In if expression0 then expression1

else expression2 fi , when changing expression0 ,

we can assume expression1

expression2 .

In if expression0 then expression1 else expression2 fi , when changing expression1 ,

we can assume expression0 .

In if expression0 then expression1 else expression2 fi , when changing expression2 ,

we can assume ¬expression0 .

In the previous subsection we proved Exercise 2(k): ¬(a ∧ ¬(a∨b)) . Here is another proof, this

time using context.

¬(a ∧ ¬(a∨b)) assume a to simplify ¬(a∨b)

= ¬(a ∧ ¬(T∨b)) Symmetry Law and Base Law for ∨

= ¬(a ∧ ¬T) Truth Table for ¬

= ¬(a ∧ ⊥⊥

⊥⊥

) Base Law for ∧

= ¬⊥⊥

⊥⊥

Binary Axiom, or Truth Table for ¬

= T

End of Context

11 1 Basic Theories

1.0.4 Formalization

We use computers to solve problems, or to provide services, or just for fun. The desired computer

behavior is usually described at first informally, in a natural language (like English), perhaps with

some diagrams, perhaps with some hand gestures, rather than formally, using mathematical

formulas (notations). In the end, the desired computer behavior is described formally as a program.

A programmer must be able to translate informal descriptions to formal ones.

A statement in a natural language can be vague, ambiguous, or subtle, and can rely on a great deal of

cultural context. This makes formalization difficult, but also necessary. We cannot possibly say

how to formalize, in general; it requires a thorough knowledge of the natural language, and is

always subject to argument. In this subsection we just point out a few pitfalls in the translation

from English to binary expressions.

The best translation may not be a one-for-one substitution of symbols for words. The same word

in different places may be translated to different symbols, and different words may be translated to

the same symbol. The words “and”, “also”, “but”, “yet”, “however”, and “moreover” might

all be translated as ∧ . Just putting things next to each other sometimes means ∧ . For example,

“They're red, ripe, and juicy, but not sweet.” becomes red ∧ ripe ∧ juicy ∧ ¬sweet .

The word “or” in English is sometimes best translated as ∨ , and sometimes as

. For example,

“They're either small or rotten.” probably includes the possibility that they're both small and rotten,

and should be translated as small ∨ rotten . But “Either we eat them or we preserve them.”

probably excludes doing both, and is best translated as eat

preserve .

The word “if” in English is sometimes best translated as ⇒ , and sometimes as = . For example,

“If it rains, we'll stay home.” probably leaves open the possibility that we might stay home even if

it doesn't rain, and should be translated as rain ⇒ home . But “If it snows, we can go skiing.”

probably also means “and if it doesn't, we can't”, and is best translated as snow = ski .

End of Formalization

End of Binary Theory

1.1 Number Theory

Number Theory, also known as arithmetic, was designed to represent quantity. In the version we

present, a

number expression is formed in the following ways.

a sequence of one or more decimal digits

∞ “infinity”

– x “minus x ”

x + y “ x plus y ”

x – y “ x minus y ”

× y “ x times y ”

x / y “ x divided by y ”

“ x to the power y ”

if a then x else y fi

where x and y are any number expressions, and a is any binary expression. The infinite number

expression ∞ will be essential when we talk about the execution time of programs. We also

introduce several new ways of forming binary expressions:

1 Basic Theories 12

x < y “ x is less than y ”

x ≤ y “ x is less than or equal to y ”

x > y “ x is greater than y ”

x ≥ y “ x is greater than or equal to y ”

x = y “ x equals y ”, “ x is equal to y ”

y “ x differs from y ”, “ x is unequal to y ”

The axioms of Number Theory are listed at the back of the book. It's a long list, but most of them

should be familiar to you already. Notice particularly the two axioms

–∞ ≤ x ≤ ∞ extremes

–∞ < x ⇒ ∞+x = ∞ absorption

Number Theory is incomplete. For example, the binary expressions 1/0 = 5 and 0 < (–1)

1/2

can

neither be proven nor disproven.

End of Number Theory

1.2 Character Theory

The simplest character expressions are written as a graphical shape enclosed by left and right

double-quotes. For example, “A” is the “capital A” character, “1” is the “one” character, and

“ ” is the “space” character. The left and right double-quote characters must be written twice,

and enclosed, like this: “““” and “””” . Character Theory is trivial. It has operators succ

(successor), pred (predecessor), and =

< ≤ > ≥ if then else fi . I leave the details of this theory

to your inclination.

End of Character Theory

All our theories use the operators = if then else fi , so their laws are listed at the back of the

book under the heading “Generic”, meaning that they are part of every theory. These laws are not

needed as axioms of Binary Theory; for example, x=x can be proven using the Completion and

Evaluation rules. But in Number Theory and other theories, they are axioms; without them we

cannot even prove 5=5 .

The operators < ≤ > ≥ apply to some, but not all, types of expression. Whenever they do apply,

their axioms, as listed under the heading “Generic” at the back of the book, go with them.

End of Basic Theories

We have talked about binary expressions, number expressions, and character expressions. In the

following chapters, we will talk about bunch expressions, set expressions, string expressions, list

expressions, function expressions, predicate expressions, relation expressions, specification

expressions, and program expressions; so many expressions. For brevity in the following

chapters, we will often omit the word “expression”, just saying binary, number, character, bunch,

set, string, list, function, predicate, relation, specification, and program, meaning in each case a type

of expression. If this bothers you, please mentally insert the word “expression” wherever you

would like it to be.

13 1 Basic Theories

剩余241页未读，继续阅读

flexlm306

粉丝: 1
资源: 22

编程理论实践：2015-9-19版

程序设计的实用理论，第二版A Practical Theory of Programming, Second Edition

Embedded Linux Primer: A Practical, Real-World Approach

stormy attaway - matlab_ a practical introduction to programming and problem

sequential convex programming

practical c++ financial programming 中文

matlab高级编程书籍推荐

Bag of Tricks and A Strong Baseline for Deep Person Re-identification

utility theory

Practical Program Repair in the Era of Large Pre-trained Language Models

matlab practical introduction programming 4th

2进制3位数过去现在将来输赢公式代码.txt

福州大学在广东2021-2024各专业最低录取分数及位次表.pdf

WordPress 集网址、资源、资讯于一体的导航类主题开心版

【Java学习】activemq消息中间件学习demo.zip

爬取淘宝热销(热门)手机支架商品信息公开透明的数据集

【目标检测数据集】斧子数据集2396张VOC+YOLO格式（含增强60%）.zip

南昌大学科学技术学院在广东2021-2024各专业最低录取分数及位次表.pdf

南京财经大学红山学院在广东2021-2024各专业最低录取分数及位次表.pdf

武昌首义学院在广东2021-2024各专业最低录取分数及位次表.pdf

【2024国赛C题】C 题农作物的种植策略思路+代码+论文V3.rar

最新资源