3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010).pdf), страница 9

an ,where a1 = f (1), . . ., an = f (n). Then ai with i ∈ {1, . . . , n} is referred to asthe i-th element in the sequence a1 . . .an . A finite sequence is a sequence ofany length n ≥ 0. A sequence of length 0 is called the empty sequence and isusually denoted by ε.2.1 Mathematical Notation25We also allow (countably) infinite sequences. An infinite sequence of elements from A is a function ξ : N → A. To exhibit the general form of aninfinite sequence ξ we typically writeξ : a0 a1 a2 .

. .if ai = f (i) for all i ∈ N. Then i is also called an index of the element ai .Given any index i, the finite sequence a0 . . . ai is called a prefix of ξ and theinfinite sequence ai ai+1 . . . is called a suffix of ξ. Prefixes and suffixes of finitesequences are defined similarly.Consider now relations R1 , R2 , . . . on A. For any finite sequence a0 . . .anof elements from A witha0 R1 a1 , a1 R2 a2 , . . ., an−1 Rn anwe write a finite chaina0 R1 a1 R2 a2 .

. .an−1 Rn an .For example, using the relations = and ≤ on Z, we may writea0 = a1 ≤ a2 ≤ a3 = a4 .We apply this notation also to infinite sequences. Thus for any infinite sequence a0 a1 a2 . . . of elements from A witha0 R1 a1 , a1 R2 a2 , a2 R3 a3 , . . .we write an infinite chaina0 R1 a1 R2 a2 R3 a3 . .

. .In this book the computations of programs are described using the chainnotation.StringsA set of symbols is often called an alphabet. A string over an alphabet A isa finite sequence of symbols from A. For example, 1+2 is a string over thealphabet {1, 2, +}. The syntactic objects considered in this book are strings.We introduce several classes of strings: expressions, assertions, programs andcorrectness formulas.We write ≡ for the syntactic identity of strings. For example, 1 + 2 ≡ 1 + 2but not 1 + 2 ≡ 2 + 1. The symbol = is used for the “semantic equality” ofobjects. For example, if + denotes integer addition then 1+2 = 2+1.262 PreliminariesThe concatenation of strings s1 and s2 yields the string s1 s2 formed byfirst writing s1 and then s2 , without intervening space.

For example, theconcatenation of 1+ and 2+0 yields 1+2+0. A string t is called a substringof a string s if there exist strings s1 and s2 such that s ≡ s1 ts2 . Since s1 ands2 may be empty, s itself is a substring of s.Note that there can be several occurrences of the same substring in a givenstring s. For example, in the string s ≡ 1 + 1 + 1 there are two occurrencesof the substring 1+ and three occurrences of the substring 1.ProofsMathematical proofs are often chains of equalities between expressions. Wepresent such chains in a special format (see, for example, Dijkstra andScholten [1990]):expression 1= {explanation why expression 1 = expression 2}expression 2...expression n − 1={explanation why expression n − 1 = expression n}expression n.An analogous format is used for other relations between assertions or expressions, such as syntactic identity ≡ of strings, inclusion ⊆ of sets, andimplications or equivalences of assertions.

Obvious explanations are sometimes omitted.Following Halmos [1985] (cf. p. 403) we use the symbol iff as an abbreviation for if and only if and the symbol ¤ to denote the end of a proof, adefinition or an example.For the conciseness of mathematical statements we sometimes use thequantifier symbols ∃ and ∀ for, respectively, there exists and for all.

Theformal definition of syntax and semantics of these quantifiers appears in Sections 2.5 and 2.6.2.1 Mathematical Notation27InductionIn this book we often use inductive definitions and proofs. We assume thatthe reader is familiar with the induction principle for natural numbers. Thisprinciple states that in order to prove a property P for all n ∈ N, it sufficesto proceed by induction on n, organizing the proof as follows:• Induction basis. Prove that P holds for n = 0.• Induction step. Prove that P holds for n + 1 from the induction hypothesisthat P holds for n.We can also use this induction principle to justify inductive definitionsbased on natural numbers. For example, consider once more the inductivedefinition of the n-fold relational composition Rn of a relation R on a set A.The implicit claim of this definition is: Rn is a well-defined relation on A forall n ∈ N.

The proof is by induction on n and is straightforward.A more interesting example is the following.Example 2.1. The inclusion Rn ⊆ R∗ holds for all n ∈ N. The proof is byinduction on n.• Induction basis. By definition, R0 = {(a, a) | a ∈ A}. Since R∗ is reflexive,R0 ⊆ R∗ follows.• Induction step. Using the proof format explained earlier, we argue as follows:Rn+1={definition of Rn+1 }nR ◦R⊆{induction hypothesis, definition of ◦}R ◦R∗⊆{definition of R∗ }R ◦ R∗∗⊆Thus Rn+1 ⊆ R∗ .{transitivity of R∗ }R∗ .⊓⊔The induction principle for natural numbers is based on the fact that thenatural numbers can be constructed by beginning with the number 0 andrepeatedly adding 1.

By allowing more general construction methods, oneobtains the principle of structural induction, enabling the use of more thanone case at the induction basis and at the induction step.For example, consider the set of (fully bracketed) arithmetic expressionswith constants 0 and 1, the variable v, and the operator symbols + and ·. This282 Preliminariesis the smallest set of strings over the alphabet {0, 1, v, +, ·, (, )} satisfying thefollowing inductive definition:• Induction basis. 0,1 and v are arithmetical expressions.• Induction step. If e1 and e2 are arithmetical expressions, then (e1 + e2 )and (e1 · e2 ) are also arithmetical expressions.Thus there are here three cases at the induction basis and two at the inductionstep.In this book we give a number of such inductive definitions; usually thekeywords “induction basis” and “induction step” are dropped. Inductive definitions form the basis for inductive proofs.Example 2.2. For an arithmetic expression e as above let c(e) denote thenumber of occurrences of constants and variables in e, and o(e) denote thenumber of occurrences of operator symbols in e.

For instance, e ≡ ((0 + v) +(v · 1)) yields c(e) = 4 and o(e) = 3. We claim thatc(e) = 1 + o(e)holds for all arithmetic expressions e.The proof is by induction on the structure of e.• Induction basis. If e ≡ 0 or e ≡ 1 or e ≡ v then c(e) = 1 and o(e) = 0.Thus c(e) = 1 + o(e).• Induction step. Suppose that e ≡ (e1 + e2 ).

Thenc(e)={definition of e}c((e1 + e2 ))={definition of c}c(e1 ) + c(e2 ){induction hypothesis}1 + o(e1 ) + 1 + o(e2 )= {definition of o}=1 + o((e1 + e2 ))= {definition of e}1 + o(e).The case when e ≡ (e1 · e2 ) is handled analogously.⊓⊔These remarks on induction are sufficient for the purposes of our book.A more detailed account on induction can be found, for example, in Loeckxand Sieber [1987].2.2 Typed Expressions29GrammarsOften the presentation of inductive definitions of sets of strings can be mademore concise by using context-free grammars in the so-called Backus-NaurForm (known as BNF).For example, we can define an arithmetic expression as a string of symbols0, 1, v, +, ·, (, ) generated by the following grammar:e ::= 0 | 1 | v | (e1 + e2 ) | (e1 · e2 ).Here the letters e, e1 , e2 are understood to range over arithmetic expressions.The metasymbol ::= reads as “is of the form” and the metasymbol | reads as“or.” Thus the above definition states that an arithmetic expression e is ofthe form 0 or 1 or v or (e1 + e2 ) or (e1 · e2 ) where e1 and e2 themselves arearithmetic expressions.In this book we use grammars to define the syntax of several classes ofprograms.2.2 Typed ExpressionsTyped expressions occur in programs on the right-hand sides of assignmentsand as subscripts of array variables.

To define them we first define the typesthat are used.TypesWe assume at least two basic types:• integer,• Boolean.Further on, for each n ≥ 1 we consider the following higher types:• T1 × . . . × Tn → T , where T1 , . . ., Tn , T are basic types. Here T1 , . . ., Tn arecalled argument types and T the value type.Occasionally other basic types such as character are used. A type should beviewed as a name, or a notation for the intended set of values. Type integerdenotes the set of all integers, type Boolean the set {true, false} and a typeT1 × . .

. × Tn → T the set of all functions from the Cartesian product of thesets denoted by T1 , . . ., Tn to the set denoted by T .302 PreliminariesVariablesWe distinguish two sorts of variables:• simple variables,• array variables or just arrays.Simple variables are of a basic type. Simple variables of type integer arecalled integer variables and are usually denoted by i, j, k, x, y, z. Simple variables of type Boolean are called Boolean variables. In programs, simple variables are usually denoted by more suggestive names such as turn or found.Array variables are of a higher type, that is, denote a function from acertain argument type into a value type. We typically use letters a, b, c forarray variables. If a is an array of type integer → T then a denotes a functionfrom the integers into the value set denoted by T .

Then for any k, l withk ≤ l the section a[k : l] stands for the restriction of a to the interval [k : l] ={i | k ≤ i ≤ l}. The number of arguments of the higher type associated withthe array a is called its dimension.We denote the set of all simple and array variables by Var.ConstantsThe value of variables can be changed during execution of a program, whereasthe value of constants remains fixed. We distinguish two sorts of constants:• constants of basic type,• constants of higher type.Among the constants of basic type we distinguish integer constants andBoolean constants.

We assume infinitely many integer constants: 0,-1,1, 2,2,. . . and two Boolean constants: true, false.Among the constants of a higher type T1 ×. . .×Tn → T we distinguish twokinds. When the value type T is Boolean, the constant is called a relationsymbol; otherwise the constant is called a function symbol; n is called thearity of the constant.We do not wish to be overly specific, but we introduce at least the followingfunction and relation symbols:••••••| | of type integer → integer,+, −, ·, min, max, div, mod of type integer × integer → integer,=int , <, divides of type integer × integer → Boolean,int of type Boolean → integer,¬ of type Boolean → Boolean,=Bool , ∨ , ∧ , → , ↔ of type Boolean × Boolean → Boolean.2.2 Typed Expressions31In the sequel we drop the subscripts when using =, since from the contextit is always clear which interpretation is meant.