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), страница 10

The value of each of the aboveconstants is as expected and is explained when discussing the semantics ofexpressions in Section 2.3.The relation symbols ¬ (negation), ∨ (disjunction), ∧ (conjunction),→ (implication) and ↔ (equivalence) are usually called connectives.This definition is slightly unusual in that we classify the nonlogical symbolsof Peano arithmetic and the connectives as constants. However, their meaningis fixed and consequently it is natural to view them as constants. This allowsus to define concisely expressions in the next section.ExpressionsOut of typed variables and constants we construct typed expressions or, inshort, expressions. We allow here only expressions of a basic type.

Thus wedistinguish integer expressions, usually denoted by letters s, t and Booleanexpressions, usually denoted by the letter B. Expressions are defined by induction as follows:• a simple variable of type T is an expression of type T ,• a constant of a basic type T is an expression of type T ,• if s1 , . . ., sn are expressions of type T1 , . . ., Tn , respectively, and op is aconstant of type T1 × . . . × Tn → T , then op(s1 , .

. ., sn ) is an expression oftype T ,• if s1 , . . ., sn are expressions of type T1 , . . ., Tn , respectively, and a is anarray of type T1 × . . . × Tn → T , then a[s1 , . . ., sn ] is an expression of typeT,• if B is a Boolean expression and s1 and s2 are expressions of type T , thenif B then s1 else s2 fi is an expression of type T .For binary constants op we mostly use the infix notation(s1 op s2 )instead of prefix notation op(s1 , s2 ). For the unary constant op ≡ ¬ it iscustomary to drop brackets around the argument, that is, to write ¬B insteadof ¬(B). In general, brackets ( and ) can be omitted if this does not lead to anyambiguities. To resolve remaining ambiguities, it is customary to introduce abinding order among the binary constants. In the following list the constantsin each line bind more strongly than those in the next line:· , mod and div,+ and −,322 Preliminaries= , < and divides,∨ and ∧ ,→ and ↔ .Thus binary function symbols bind more strongly than binary relation symbols.

Symbols of stronger binding power are bracketed first. For example, theexpression x + y mod z is interpreted as x + (y mod z) and the assertionp ∧ q → r is interpreted as (p ∧ q) → r.Example 2.3. Suppose that a is an array of type integer × Boolean →Boolean, x an integer variable, f ound a Boolean variable and B a Booleanexpression. Then B ∨ a[x + 1, f ound] is a Boolean expression and so is a[2 ·x, a[x, ¬f ound]], whereas int(a[x, ¬B]) is an integer expression.

In contrast,a[f ound, f ound] is not an expression and neither is a[x, x].⊓⊔By a subexpression of an expression s we mean a substring of s that isagain an expression. By var(s) for an expression s we denote the set of allsimple and array variables that occur in s.Subscripted VariablesExpressions of the form a[s1 , . . ., sn ] are called subscripted variables. Subscripted variables are somewhat unusual objects from the point of view oflogic. They are called variables because, together with simple variables, theycan be assigned a value in programs by means of an assignment statement,which is discussed in the next chapter.

Also, they can be substituted for (seeSection 2.7). However, they cannot be quantified over (see Section 2.5) andtheir value cannot be fixed in a direct way (see Section 2.3). Assignments toa subscripted variable a[s1 , . . ., sn ] model a selected update of the array a atthe argument tuple [s1 , . . ., sn ].In the following simple and subscripted variables are usually denoted bythe letters u, v.2.3 Semantics of ExpressionsIn general a semantics is a mapping assigning to each element of a syntacticdomain some value drawn from a semantic domain. In this section we explainthe semantics of expressions.2.3 Semantics of Expressions33Fixed StructureFrom logic we need the notion of a structure: this is a pair S = (D, I) where• D is a nonempty set of data or values called a semantic domain.

We usethe letter d as typical element of D.• I is an interpretation of the constants, that is, a mapping that assigns toeach constant c a value I(c) from D. We say that the constant c denotesthe value I(c).In contrast to general studies in logic we stipulate a fixed structure S throughout this book. Its semantic domain D is the disjoint union[D=DT ,T is a typewhere for each T the corresponding semantic domain DT is defined inductively as follows:• Dinteger = Z, the set of integers,• DBoolean = {true, false}, the set of Boolean values,• DT1 ×. . .×Tn → T = DT1 × .

. . × DTn → DT , the set of all functions from theCartesian product of the sets DT1 , . . ., DTn into the set DT .The interpretation I is defined as follows: each constant c of base type denotesitself, that is, I(c) = c; each constant op of higher type denotes a fixedfunction I(op).For example, the integer constant 1 denotes the integer number 1 and theBoolean constant true denotes the Boolean value true. The unary constant| | denotes the absolute value function. The unary constant ¬ denotes thenegation of Boolean values:¬(true) = false and ¬(false) = true.The binary constants div and mod are written in infix form and denote integerdivision and remainder defined uniquely by the following requirements:(x div y) · y + x mod y = x,0 ≤ x mod y < y for y > 0,y < x mod y ≤ 0 for y < 0.To ensure that these functions are total we additionally stipulatex div 0 = 0 and x mod 0 = xfor the special case of y = 0.342 PreliminariesThe binary constant divides is defined byx divides y iff y mod x = 0.The unary constant int denotes the function withint(true) = 1 and int(false) = 0.StatesIn contrast to constants, the value of variables is not fixed but given throughso-called proper states.

A proper state is a mapping that assigns to everysimple and array variable of type T a value in the domain DT . We use theletter Σ to denote the set of proper states.Example 2.4. Let a be an array of type integer × Boolean → Booleanand x be an integer variable. Then each state σ assigns to a a functionσ(a) : {..., −1, 0, 1, ...} × {true, false} → {true, false}and to x a value from {..., −1, 0, 1, ...}.

For example, σ(a)(5, true) ∈{true, false} and σ(a)(σ(x), false) ∈ {true, false}.⊓⊔Later, in Section 2.6, we also use three error states representing abnormalsituations in a program execution: ⊥ denotes divergence of a program, faildenotes a failure in an execution of a program and ∆ denotes a deadlock in anexecution of a program. These error states are just special symbols and notmappings from variables to data values as proper states; they are introducedin Chapters 3, 9 and 10, respectively.By a state we mean a proper or an error state.

States are denoted by theletters σ, τ, ρ.Let Z ⊆ V ar be a set of simple or array variables. Then we denote byσ[Z] the restriction of a proper state σ to the variables occurring in Z. Byconvention, for error states we define ⊥[Z] = ⊥, and similarly for ∆ and fail.We say that two sets of states X and Y agree modulo Z, and writeX = Y mod Z,if{σ[Var − Z] | σ ∈ X} = {σ[Var − Z] | σ ∈ Y }.By the above convention, X = Y mod Z implies the following for errorstates: ⊥ ∈ X iff ⊥ ∈ Y , ∆ ∈ X iff ∆ ∈ Y and fail ∈ X iff fail ∈ Y . Forsingleton sets X, Y , and Z we omit the brackets { and } around the singletonelement. For example, for proper states σ, τ and a simple variable x,2.3 Semantics of Expressions35σ = τ mod xstates that σ and τ agree modulo x, i.e., for all simple and array variablesv ∈ V ar with v 6= x we have σ(v) = τ (v).Definition of the SemanticsThe semantics of an expression s of type T in the structure S is a mappingS[[s]] : Σ → DTwhich assigns to s a value S[[s]](σ) from DT depending on a given properstate σ.

This mapping is defined by induction on the structure of s:• if s is a simple variable thenS[[s]](σ) = σ(s),• if s is a constant of a basic type denoting the value d, thenS[[s]](σ) = d,• if s ≡ op(s1 , . . ., sn ) for some constant op of higher type denoting a functionf thenS[[s]](σ) = f (S[[s1 ]](σ), . . ., S[[sn ]](σ)),• if s ≡ a[s1 , .

. ., sn ] for some array variable a thenS[[s]](σ) = σ(a)(S[[s1 ]](σ), . . ., S[[sn ]](σ)),• if s ≡ if B then s1 else s2 fi for some Boolean expression B then½S[[s1 ]](σ) if S[[B]](σ) = true,S[[s]](σ) =S[[s2 ]](σ) if S[[B]](σ) = false,• if s ≡ (s1 ) thenS[[s]](σ) = S[[s1 ]](σ).Since S is fixed throughout this book, we abbreviate the standard notionS[[s]](σ) from logic to σ(s).

We extend this notation and apply states also tolists of expressions: for a list s̄ = s1 , . . . , sn of expressions σ(s̄) denotes thelist of values σ(s1 ), . . . , σ(sn ).Example 2.5.(a) Let a be an array of type integer → integer. Then for any proper stateσ we have σ(1 + 1) = σ(1) + σ(1) = 1 + 1 = 2; so362 Preliminariesσ(a[1 + 1]) = σ(a)(σ(1 + 1)) = σ(a)(2) = σ(a[2]),thus a[1 + 1] and a[2] have the same value in all proper states, as desired.(b) Consider now a proper state σ with σ(x) = 1 and σ(a)(1) = 2. Thenσ(a[a[x]])= {definition of σ(s)}σ(a)(σ(a)(σ(x)))= {σ(x) = 1, σ(a)(1) = 2}σ(a)(2)= σ(a[2])andσ(a[if x = 1 then 2 else b[x] fi])={definition of σ(s)}σ(a)(σ(if x = 1 then 2 else b[x] fi))={σ(x) = 1, definition of σ(s)}σ(a)(σ(2))= σ(a[2]).⊓⊔Updates of StatesFor the semantics of assignments we need in the sequel the notion of anupdate of a proper state σ, written as σ[u := d], where u is a simple orsubscripted variable of type T and d is an element of type T .