3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 8
Текст из файла (страница 8)
. . . . . . . . . . . . . . . . . . . . . . . . . . . .Typed Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics of Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Formal Proof Systems . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . .Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics of Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . .Substitution Lemma . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Bibliographic Remarks . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . .21293238394142475051N THIS CHAPTER we explain the basic concepts and notations usedthroughout this book. We recommend to the reader to move now toChapter 3 and consult the individual sections of this chapter wheneverneeded.This chapter is organized as follows. In Section 2.1, we list the standardmathematical notation for sets, tuples, relations, functions, sequences, strings,proofs, induction and grammars.Section 2.2 is needed to understand the syntax of the programs studied inthis book.
For the operational semantics of all considered classes of programs,Sections 2.3 and 2.4 are needed. For the verification of programs, in particularfor the definition of correctness formulas, Sections 2.5 and 2.6 on assertionsand Section 2.7 on substitution are needed. The introduction of proof systems19202 Preliminariesfor program verification assumes again knowledge of Section 2.4. Finally, toshow the soundness of these proof systems the Substitution Lemma introduced in Section 2.8 is needed.2.1 Mathematical Notation212.1 Mathematical NotationSetsWe assume the reader is familiar with the notion of a set, a collection ofelements. Finite sets may be specified by enumerating their elements betweencurly brackets.
For example, {true, false} denotes the set consisting of theBoolean constants true and false. When enumerating the elements of a set,we sometimes use “. . .” as a notation. For example, {1, . . ., n} denotes theset consisting of the natural numbers 1, . . ., n where the upper bound n is anatural number that is not further specified.More generally, sets are specified by referring to some property of theirelements:{x | P }denotes the set consisting of all elements x that satisfy the property P . Forexample,{x | x is an integer and x is divisible by 2}denotes the infinite set of all even integers.We write a ∈ A to denote that a is an element of the set A, and b 6∈ Ato denote that b is not an element of A. Sometimes it is convenient to referto a given set A when defining a new set.
We write{x ∈ A | P }as an abbreviation for {x | x ∈ A and P }.Some sets have standard names: ∅ denotes the empty set, N denotes theset of all natural numbers {0, 1, 2, 3, . . . }, and Z denotes the set of all integers{. . . , −1, 0, 1, 2, . . . }. Connected subsets of integers are called intervals. Fork, l ∈ Z the closed interval of integers between k and l is defined by[k : l] = {i ∈ Z | k ≤ i ≤ l},and the open interval by (k : l) = {i ∈ Z | k < i < l}.
Half-open intervalslike (k : l] or [k : l) are defined analogously.Recall that in a set one does not distinguish repetitions of elements. Thus{true, false} and {true, false, true} are the same set. Similarly, the orderof elements is irrelevant. Thus {true, false} and {false, true} are the sameset. In general, two sets A and B are equal (i.e., the same) if and only if theyhave the same elements; in symbols: A = B.Let A and B be sets.
Then A ⊆ B (and B ⊇ A) denotes that A is a subsetof B, A ∩ B denotes the intersection of A and B, A ∪ B the union of A andB, and A − B the set difference of A and B. In other words,A ⊆ B if a ∈ B for every a ∈ A,222 PreliminariesA ∩ B = {a | a ∈ A and b ∈ B},A ∪ B = {a | a ∈ A or b ∈ B},A − B = {a | a ∈ A and b 6∈ B}.Note that A = B if both A ⊆ B and A ⊇ B.
A and B are disjoint if theyhave no element in common, that is, if A ∩ B = ∅.The definitions of intersection and union can be generalized to the case ofmore than two sets. Let Ai be a set for every element i of some other set I.ThenTSi∈I Ai = {a | a ∈ Ai for all i ∈ I},i∈I Ai = {a | a ∈ Ai for some i ∈ I}.For a finite set A, card A denotes the cardinality, or the number of elements,of A. For a nonempty finite set A ⊆ Z let min A denote the minimum of allintegers in A.
Finally, for a set A we define P(A) = {B | B ⊆ A}.TuplesIn sets the repetition of elements and their order is irrelevant. If these thingsmatter, we use another way of grouping elements: ordered pairs and tuples.For elements a and b, not necessarily distinct, (a, b) is an ordered pair orsimply pair. Then a and b are called the components of (a, b). By definition,two pairs (a, b) and (c, d) are identical if and only if their first componentsand their second components agree.
In symbols: (a, b) = (c, d) if and only ifa = c and b = d. Sometimes we use angle brackets and write pairs as < a, b >.More generally, let n be any natural number. Then if a1 , . . ., an are anyn elements, not necessarily distinct, (a1 , . . ., an ) is an n-tuple. The elementai , where i ∈ {1, . . . , n}, is called the i-th component of (a1 , . . ., an ) . An ntuple (a1 , . . ., an ) is equal to an m-tuple (b1 , . . ., bm ) if and only if n = m andai = bi for all i ∈ {1, . .
. , n}. For example, the tuples (1,1), (1,1,1), ((1,1),1)and (1,(1,1)) are all distinct. Note that 2-tuples are the same as pairs. Asborder cases, we also obtain the 0-tuple, written as (), and 1-tuples (a1 ) forany element a1 .The Cartesian product A × B of sets A and B consists of all pairs (a, b)with a ∈ A and b ∈ B. The n-fold Cartesian product A1 × · · · × An of setsA1 , . .
., An consists of all n-tuples (a1 , . . ., an ) with ai ∈ Ai for i ∈ {1, . . . , n}.If all the Ai are the same set A, the n-fold Cartesian product A × · · · × A ofA with itself is also written as An .2.1 Mathematical Notation23RelationsA binary relation R between sets A and B is a subset of the Cartesian productA × B; that is, R ⊆ A × B. If A = B then R is called a relation on A. Forexample,{(a, 1), (b, 2), (c, 2)}is a binary relation between {a, b, c} and {1, 2}. More generally, for any natural number n an n-ary relation R between A1 , .
. ., An is a subset of the n-foldCartesian product A1 × · · · × An ; that is, R ⊆ A1 × · · · × An . Note that 2-aryrelations are the same as binary relations. Instead of 1-ary and 3-ary relationsone usually talks of unary and ternary relations.Consider a relation R on a set A. R is called reflexive if (a, a) ∈ R forall a ∈ A; it is called irreflexive if (a, a) 6∈ R for all a ∈ A. R is calledsymmetric if for all a, b ∈ A whenever (a, b) ∈ R then also (b, a) ∈ R; it iscalled antisymmetric if for all a, b ∈ A whenever (a, b) ∈ R and (b, a) ∈ Rthen a = b. R is called transitive if for all a, b, c ∈ A whenever (a, b) ∈ R and(b, c) ∈ R then also (a, c) ∈ R.The transitive, reflexive closure R∗ of a relation R on a set A is the smallest transitive and reflexive relation on A that contains R as a subset.
Therelational composition R1 ◦ R2 of relations R1 and R2 on a set A is definedas follows:R1 ◦ R2 = {(a, c) | there exists b ∈ A with (a, b) ∈ R1 and (b, c) ∈ R2 }.For any natural number n the n-fold relational composition Rn of a relationR on a set A is defined inductively as follows:R0 = {(a, a) | a ∈ A},Rn+1 = Rn ◦ R.Note thatR∗ = ∪ n∈N Rn .Membership of pairs in a binary relation R is mostly written in infix notation, so instead of (a, b) ∈ R one usually writes aR b.Any binary relation R ⊆ A × B has an inverse R−1 ⊆ B × A defined asfollows:b R−1 a if aR b.FunctionsLet A and B be sets. A function or mapping from A to B is a binary relationf between A and B with the following special property: for each element242 Preliminariesa ∈ A there is exactly one element b ∈ B with af b.
Mostly we use prefixnotation for function application and write f (a) = b instead of af b. For somefunctions, however, we use postfix notation and write af = b. An example issubstitution as defined in Section 2.7. In both cases b is called the value of fapplied to the argument a. To indicate that f is a function from A to B wewritef : A → B.The set A is called the domain of f and the set B the co-domain of f .Consider a function f : A → B and some set X ⊆ A. Then the restrictionof f to X is denoted by f [X] and defined as the intersection of f (which is asubset of A × B) with X × B:f [X] = f ∩ (X × B).We are sometimes interested in functions with special properties.
A functionf : A → B is called one-to-one or injective if f (a1 ) 6= f (a2 ) for any twodistinct elements a1 , a2 ∈ A; it is called onto or surjective if for every elementb ∈ B there exists an element a ∈ A with f (a) = b; it is called bijective or abijection from A onto B if it is both injective and surjective.Consider a function whose domain is a Cartesian product, say f : A1 ×· · · × An → B.
Then it is customary to drop one pair of parentheses whenapplying f to an element (a1 , . . ., an ) ∈ A1 × · · · × An . That is, we writef (a1 , . . ., an )for the value of f at (a1 , . . ., an ) rather than f ((a1 , . . ., an )). We also say thatf is an n-ary function. If f (a1 , . . ., an ) = b then b is called the value of fwhen applied to the arguments a1 , . .
., an .Consider a function whose domain and co-domain coincide, say f : A → A.An element a ∈ A is called a fixed point of f if f (a) = a.SequencesIn the following let A be a set. A sequence of elements from A of length n ≥ 0is a function f : {1, . . ., n} → A. We write a sequence f by listing the valuesof f without any sort of punctuation in the order of ascending arguments,that is, asa1 . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
