3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 29
Текст из файла (страница 29)
Therefore we definechange(begin local x̄ := t̄; S1 end) = change(S1 ) \ {x̄}.Additionally, the procedure calls with parameters are introduced by thefollowing clause:S ::= P (t1 , . . . , tn ).Here P is a procedure identifier and t1 , . . . , tn are expressions called actual parameters. To ensure that our analysis generalizes that of the previous chapterwe assume that n ≥ 0. When n = 0 the procedure P has no actual parameters and we are within the framework of the previous chapter. The statementP (t1 , . . . , tn ) is called a procedure call .Procedures are now defined by declarations of the formP (u1 , . . .
, un ) :: S.Here u1 , . . . , un are distinct simple variables, called formal parameters of theprocedure P , and S is the body of the procedure P . From now on, as in theprevious chapter, we assume a given set of procedure declarations D suchthat each procedure that appears in D has a unique declaration in D.A recursive program consists of a main statement S built according to thesyntax of this section and a given set D of such procedure declarations.
Weassume as in the previous chapter that all procedures whose calls appear inthe main statement are declared in D. Additionally, we assume now that theprocedure calls are well-typed, which means that the numbers of formal and5.1 Syntax153actual parameters agree and that for each parameter position the types ofthe corresponding actual and formal parameters coincide. If D is clear fromthe context we refer to the main statement as a recursive program.Given a recursive program, we call a variable xi local if it appears withina statement S such that begin local x̄ := t̄; S end with x̄ = x1 , .
. ., xk is asubstatement of the main statement or of one of its procedure bodies, andglobal otherwise. To avoid possible name clashes between local and globalvariables of a program we simply assume that these sets of variables aredisjoint. So given the procedure declarationP :: if x = 1 then b := true else b := false fithe main statementS ≡ begin local x := 1; P endis not allowed. If it were, the semantics we are about to introduce would allowus to conclude that {x = 0} S {b} holds.
However, the customary semanticsof the programs in the presence of procedures prescribes that in this case{x = 0} S {¬b} should hold, as the meaning of a program should not dependon the choice of the names of its local variables. (This is a consequence of theso-called static scope of the variables that we assume here.)This problem is trivially solved by just renaming the ‘offensive’ local variables to avoid name clashes, so by considering here the programbegin local y := 1; P end instead.
In what follows, when considering a recursive program S in the context of a set of procedure declarations D wealways implicitly assume that the above syntactic restriction is satisfied.Note that the above definition of programs puts no restrictions on theactual parameters in procedure calls; in particular they can be formal parameters or global variables. Let us look at an example.Example 5.1. Using recursive programs with parameters, the factorial procedure from Example 4.1 can be rewritten as follows:F ac(u) :: if u = 0 then y := 1 else F ac(u − 1); y := y · u fi.(5.1)Here u is a formal parameter, u − 1 is an actual parameter, while y is a globalvariable.⊓⊔The above version of the factorial procedure does not use any local variables.
The procedure below does.Example 5.2. Consider the following procedure Ct, standing for ‘Countdown’:Ct(u) :: begin local v := u − 1; if v 6= 0 then Ct(v) fi end.(5.2)1545 Recursive Programs with ParametersHere v is a local variable and is also used as an actual parameter. Thisprocedure has no global variables.⊓⊔So far we did not clarify why the block statement is needed when considering procedures with parameters. Also, we did not discuss the initializationof local variables. We shall consider these matters after having provided semantics to the considered class of programs.5.2 SemanticsIn order to define the semantics of the considered programs we extend thetransition system of the previous chapter to take care of the block statementand of the procedure calls in the presence of parameters.
The transition axiomfor the block statement, given below, ensures that• the local variables are initialized as prescribed by the parallel assignment,• upon termination, the global variables whose names coincide with the localvariables are restored to their initial values, held at the beginning of theblock statement.(ix) < begin local x̄ := t̄; S end, σ > → < x̄ := t̄; S; x̄ := σ(x̄), σ >.From now on, to ensure a uniform presentation for the procedures with andwithout parameters we identify the statement begin local ū := t̄; S end,when ū is the empty sequence, with S.
We then add the following transitionaxiom that deals with the procedure calls with parameters:(x) < P (t̄), σ > → < begin local ū := t̄; S end, σ >,where P (ū) :: S ∈ D.So when the procedure P has no parameters, this transition axiom reducesto the transition axiom (viii).In this axiom the formal parameters are simultaneously instantiated tothe actual parameters and subsequently the procedure body is executed. Ingeneral, it is crucial that the passing of the values of the actual parametersto the formal ones takes place by means of a parallel assignment and not bya sequence of assignments. For example, given a procedure P (u1 , u2 ) :: S andthe call P (u1 + 1, u1 ), the parallel assignment u1 , u2 := u1 + 1, u1 assigns adifferent value to the formal parameter u2 than the sequenceu1 := u1 + 1; u2 := u1 .The block statement is needed to limit the scope of the formal parametersso that they are not accessible after termination of the procedure call.
Alsoit ensures that the values of the formal parameters are not changed by aprocedure call: note that, thanks to the semantics of a block statement, upon5.2 Semantics155termination of a procedure call the formal parameters are restored to theirinitial values.This transition axiom clarifies that we consider here the call-by-value parameter mechanism, that is, the values of the actual parameters are assignedto the formal parameters.The following example illustrates the uses of the new transition axioms.Example 5.3.
Assume the declaration (5.1) of the Fac procedure. Then wehave the following computation of the main statement F ac(x), where σ is aproper state with σ(x) = 2:< F ac(x), σ >→ < begin local u := x;if u = 0 then y := 1 else F ac(u − 1); y := y · u fi end, σ >→ < u := x; if u = 0 then y := 1 else F ac(u − 1); y := y · u fi;u := σ(u), σ >→ < if u = 0 then y := 1 else F ac(u − 1); y := y · u fi;u := σ(u), σ[u := 2] >→ < F ac(u − 1); y := y · u; u := σ(u), σ[u := 2] >→ < begin local u := u − 1;if u = 0 then y := 1 else F ac(u − 1); y := y · u fi end;y := y · u; u := σ(u), σ[u := 2] >→ < u := u − 1; if u = 0 then y := 1 else F ac(u − 1); y := y · u fi;u := 2; y := y · u; u := σ(u), σ[u := 2] >→ < if u = 0 then y := 1 else F ac(u − 1); y := y · u fi;u := 2; y := y · u; u := σ(u), σ[u := 1] >→ < F ac(u − 1); y := y · u; u := 2; y := y · u; u := σ(u), σ[u := 1] >→ < begin local u := u − 1;if u = 0 then y := 1 else F ac(u − 1); y := y · u fi end;y := y · u; u := 2; y := y · u; u := σ(u), σ[u := 1] >→ < u := u − 1; if u = 0 then y := 1 else F ac(u − 1); y := y · u fi;u := 1; y := y · u; u := 2; y := y · u; u := σ(u), σ[u := 1] >→ < if u = 0 then y := 1 else F ac(u − 1); y := y · u fi; u := 1;y := y · u; u := 2; y := y · u; u := σ(u), σ[u := 0] >→ < y := 1; u := 1; y := y · u; u := 2; y := y · u; u := σ(u), σ[u := 0] >→ < u := 1; y := y · u; u := 2; y := y · u; u := σ(u), σ[u, y := 0, 1] >→ < y := y · u; u := 2; y := y · u; u := σ(u), σ[u, y := 1, 1] >→ < u := 2; y := y · u; u := σ(u), σ[u, y := 1, 1] >→ < y := y · u; u := σ(u), σ[u, y := 2, 1] >→ < u := σ(u), σ[u, y := 2, 2] >→ < E, σ[y := 2] >⊓⊔So in the above example during the computation of the procedure callF ac(x) block statements of the form begin local u := u − 1; S end are in-1565 Recursive Programs with Parameterstroduced.
The assignments u := u − 1 result from the calls F ac(u − 1) andare used to instantiate the formal parameter u to the value of the actualparameter u − 1 that refers to a global variable u.In general, block statements of the form begin local x̄ := t̄; S end, inwhich some variables from x̄ appear in t̄, arise in computations of the recursiveprograms in which for some procedures some formal parameters appear inan actual parameter. Such block statements also arise in reasoning aboutprocedure calls.Exercise 5.1 shows that once we stipulate that actual parameters do notcontain formal parameters, such block statements cannot arise in the computations. We do not impose this restriction on our programs since this leadsto a limited class of recursive programs.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
