ACSL-by-Example книга со спецификациями на frama-c всех стандартных алгоритмов (1184405), страница 3
Текст из файла (страница 3)
Since overflows are detected using this integer model, one should selectit, whenever one wishes to prevent overflow.• modulo, which allows for overflow. If an overflow occurs, the value is taken modulo 2n ,where n is the number of bits of the specific type.Selection and invocation of a particular integer-model should be considered when generating verification conditions. This can be expressed using the following option:frama-c -jessie -jessie-int-model model filenameBy default, if no specific model is set, the bounded integer model is assumed for the generationof verification conditions. Note: All of the examples in this tutorial used the default integer model.Separation of Memory RegionsSome algorithms in this tutorial, e.g. copy (see Section 6.5), require that the memory regionsreferenced by different pointers do not overlap.
One way to deal with this problem in Jessieconsists in using pragmas that specify different separation policies.6#pragma SeparationPolicy(value)By default, Jessie assumes that different pointers point into different memory regions. We applythis policy for algorithm like copy since by definition different memory regions do not overlap.6For more details we refer to the Jessie tutorial[13, Chapter 5].10The #pragma SeparationPolicy(none) means that different pointer arguments can pointto the same region of memory. Normally, we apply this separation policy because it correspondsto the C Standard.112. The Hoare CalculusIn 1969, C.A.R.
Hoare introduced a calculus for formal reasoning about properties of imperativeprograms [14], which became known as “Hoare Calculus”.The basic notion is//@ PQ//@ Rwhere P and R denote logical expressions and Q denotes a source-code fragment. Informally, thismeans “If P holds before the execution of Q, then R will hold after the execution”.
Usually, Pand R are called “precondition” and “postcondition” of Q, respectively. The syntax for logicalexpressions is described in [10, Section 2.2] in full detail. For the purposes of this tutorial, thenotions shown in Table 2.1 are sufficient.
Note that they closely resemble the logical and relationaloperators in C.!PP && QP || QP ==> QP <==> Qx < y == z\forall int x; P(x)\exists int x; P(x)negationconjunctiondisjunctionimplicationequivalencerelation chainuniversal quantifierexistential quantifier“P is not true”“P is true and Q is true”“P is true or Q is true”“if P is true, then Q is true”“if, and only if, P is true, then Q is true”“x is less than y and y is equal to z”“P(x) is true for every int value of x”“P(x) is true for some int value of x”Table 2.1.: Some ACSL formula syntax//@ x % 2 == 1++x;//@ x % 2 == 0//@ 0 <= x <= y++x;//@ 0 <= x <= y + 1(a)(b)//@ truewhile (--x != 0)sum += a[x];//@ x == 0(c)Figure 2.2.: Example source-code fragments and annotationsFigure 2.2 shows three example source-code fragments and annotations.
Their informal meaningsare as follows:(a) “If x has an odd value before execution of the code ++x then x has an even value thereafter.”13(b) “If the value of x is in the range {0, . . . , y} before execution of the same code, then x’s valueis in the range {0, . . . , y + 1} after execution.”(c) “Under any circumstances, the value of x is zero after execution of the loop code.”Any C programmer will confirm that these properties are valid.
The examples were chosen todemonstrate also the following issues:• For a given code fragment, there does not exist one fixed pre- or postcondition. Rather,the choice of formulas depends on the actual property to be verified, which comes from theapplication context. Examples (a) and (b) share the same code fragment, but have differentpre- and postconditions.• The postcondition need not be the most restricting possible formula that can be derived. Inexample (b), it is not an error that we stated only that 0 <= x although we know that even1 <= x.• In particular, pre- and postconditions need not contain all variables appearing in the codefragment.
Neither sum nor a[] is referenced in the formulas of example (c).• We can use the predicate true to denote the absence of a properly restricting precondition,as we did in example (c).• It is not possible to express by pre- and postconditions that a given piece of code will alwaysterminate.
Example (c) only states that if the loop terminates, then x == 0 will hold. Infact, if x has a negative value on entry, the loop will run forever. However, if the loopterminates, x == 0 will hold, and that is what example (c) claims.Usually, termination issues are dealt with separately from correctness issues.
Terminationproofs may, however, refer to properties stated (and verified) using the Hoare Calculus.Hoare provided the rules shown in Figures 2.3 to 2.11 in order to reason about programs. We willcomment on them in the following sections.2.1. The Assignment RuleWe start with the rule that is probably the least intuitive of all Hoare-Calculus rules, viz. theassignment rule.
It is depicted in Figure 2.3, where “P {x7→e}” denotes the result of substitutingeach occurrence of x in P by e.//@ P {x |--> e}x = e//@ PFigure 2.3.: The assignment rule14For example,ifthenPP {x7→x+1}isis0 <= x <= 5 ==> a[2* x ] == 00 <=x+1<= 5 ==> a[2*(x+1)] == 0,.Hence, we get Figure 2.4 as an example instance of the assignment rule. Note that parentheses arerequired in the index expression to get the correct 2*(x+1) rather than the faulty 2*x+1.//@ x+1 > 0 && a[2*(x+1)] == 0x = x+1//@ x > 0 && a[2*x] == 0Figure 2.4.: An assignment rule example instanceWhen first confronted with Hoare’s assignment rule, most people are tempted to think of a simpler and more intuitive alternative, shown in Figure 2.5.
Figures 2.6.(a)–(c) show some exampleinstances.//@ Px = e//@ P && x==eFigure 2.5.: Simpler, but faulty assignment rule//@ y > 0x = y+1//@ y>0 && x==y+1//@ truex = x+1//@ x==x+1//@ x < 0x = 5//@ x<0 && x==5(a)(b)(c)Figure 2.6.: Some example instances of the faulty rule from Figure 2.5While (a) happens to be ok, (b) and (c) lead to postconditions that are obviously nonsensicalformulas. The reason is that in the assignment in (b) the left-hand side variable x also appears inthe right-hand side expression e, while the assignment in (c) just destroys the property from itsprecondition. Note that the correct example (a) can as well be obtained as an instance of the correctrule from Figure 2.3, since replacing x by y+1 in its postcondition yields y>0 && y+1 == y+1as precondition, which is logically equivalent to just y>0.152.2.
The Sequence RuleThe sequence rule, shown in Figure 2.7, combines two code fragments Q and S into a single oneQ ; S. Note that the postcondition for Q must be identical to the precondition of S. This justreflects the sequential execution (“first do Q, then do S”) on a formal level. Thanks to this rule, wemay “annotate” a program with interspersed formulas, as it is done in Frama-C.//@ PQ//@ Rand//@ RS//@ T//@ PQ ; S//@ T{Figure 2.7.: The sequence rule2.3.
The Implication RuleThe implication rule, shown in Figure 2.8, allows us at any time to weaken a postcondition and tosharpen a precondition. We will provide application examples together with the next rule.//@ PQ//@ R{//@ P’Q//@ R’ifandP’ ==> PR ==> R’Figure 2.8.: The implication rule2.4. The Choice RuleThe choice rule, depicted in Figure 2.9, is needed to verify if(...){...}else{...} statements. Both branches must establish the same postcondition, viz. S.
The implication rule can beused to weaken differing postconditions S1 of a then branch and S2 of an else branch into aunified postcondition S1||S2, if necessary. In each branch, we may use what we know aboutthe condition B, e.g. in the else branch, that it is false. If the else branch is missing, it can beconsidered as consisting of an empty sequence, having the postcondition P && !B.Figure 2.10 shows an example application of the choice rule. The variable i may be used as anindex into a ring buffer int a[n]. The shown code fragment just advances the index i appropriately.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
