ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 15
Текст из файла (страница 15)
Inheritance combined with visibility and modularity account fora number of complex features in JML (e.g, spec_public modifier, data groups, representsclauses, etc), that are necessary to express the desired inheritance-related specifications whilerespecting visibility and modularity. Since C has no inheritance, these intricacies are avoidedin ACSL.Error handling without exceptionsThe usual way of signaling errors in Java is through exceptions. Therefore, JML specificationsare tailored to express exceptional postconditions, depending on the exception raised. SinceC has no exceptions, ACSL does not use exceptional specifications.
Instead, C programmersare used to signal errors by returning special values, like mandated in various ways in the Cstandard.Example A.1 In §7.12.1 of the standard, it is said that functions in <math.h> signal errorsas follows: “On a domain error, [...] the integer expression errno acquires the value EDOM.”Example A.2 In §7.19.5.1 of the standard, it is said that function fclose signals errors asfollows: “The fclose function returns [...] EOF if any errors were detected.”Example A.3 In §7.19.6.1 of the standard, it is said that function fprintf signals errors asfollows: “The fprintf function returns [...] a negative value if an output or encoding erroroccured.”Example A.4 In §7.20.3 of the standard, it is said that memory management functionssignal errors as follows: “If the space cannot be allocated, a null pointer is returned.”86A.2.
COMPARISON WITH JMLAs shown by these few examples, there is no unique way to signal errors in the C standardlibrary, not mentioning user-defined functions. But since errors are signaled by returningspecial values, it is sufficient to write an appropriate postcondition:/*@ ensures \result == error_value || normal_postcondition; */C contracts are not Java onesIn Java, the precondition of the following function that nullifies an array of characters isalways true. Even if there was a precondition on the length of array a, it could easily beexpressed using the Java expression a.length that gives the dynamic length of array a.123456public static void Java_nullify(char[] a) {if (a == null) return;for (int i = 0; i < a.length; ++i) {a[i] = 0;}}On the contrary, the precondition of the same function in C, whose definition follows, is moreinvolved.
First, remark that the C programmer has to add an extra argument for the size ofthe array, or rather a lower bound on this array size.1234567void C_nullify(char* a, unsigned int n) {int i;if (n == 0) return;for (i = 0; i < n; ++i) {a[i] = 0;}}A correct precondition for this function is the following:/*@ requires \valid (a + 0..(n-1)); */where predicate \valid is the one defined in Section 2.7.1. (note that \valid (a + 0..(-1)) isthe same as \valid (\empty) and thus is true regardless of the validity of a itself).
When n isnull, a does not need to be valid at all, and when n is strictly positive, a must point to anarray of size at least n. To make it more obvious, the C programmer adopted a defensiveprogramming style, which returns immediately when n is null. We can duplicate this in thespecification:/*@ requires n == 0 || \valid(a + 0..(n-1)); */Usually, many memory requirements are only necessary for some paths through the function,which correspond to some particular behaviors, selected according to some tests performedalong the corresponding paths.
Since C has no memory primitives, these tests involve othervariables that the C programmer added to track additional information, like n in our example.To make it easier, it is possible in ACSL to distinguish between the assumes part of a behavior,that specifies the tests that need to succeed for this behavior to apply, and the requires partthat specifies the additional preconditions that must be true when a behavior applies.
Thespecification for our example can then be translated into:123/*@ behavior n_is_null:@ assumes n == 0;@ behavior n_is_not_null:87APPENDIX A. APPENDICES456@ assumes n > 0;@requires \valid (a + 0..(n-1));@*/This is equivalent to the previous requirement, except here behaviors can be completed withpostconditions that belong to one behavior only. Contrary to JML, the set of behaviorsfor a function do not necessarily cover all cases of use for this function, as mentioned inSection 2.3.3.
This allows for partial specifications, whereas JML behaviors cannot offersuch flexibility. Here, Our two behaviors are clearly mutually exclusive, and, since n is anunsigned int , our they cover all the possible cases. We could have specified that as well, byadding the following lines in the contract (see Section 2.3.3).1234@ ...@ disjoint behaviors ;@ complete behaviors ;@*/ACSL contracts vs. JML onesTo fully understand the difference between specifications in ACSL and JML, we detail in belowthe requirement on the pre-state and the guarantee on the post-state given by behaviors inJML and ACSL.A JML contract is either lightweight or heavyweight.
For the purpose of our comparison, it issufficient to know that a lightweight contract has requires and ensures clauses all at the samelevel, while an heavyweight contract has multiple behaviors, each consisting of requires andensures clauses. Although it is not possible in JML to mix both styles, we can define herewhat it would mean to have both, by conjoining the conditions on the pre- and the post-state.Here is an hypothetical JML contract mixing lightweight and heavyweight styles:12345678910111213/*@ requires P1 ;@ requires P2 ;@ ensures Q1 ;@ ensures Q2 ;@ behavior x1 :@requires A1 ;@requires R1 ;@ensures E1 ;@ behavior x2 :@requires A2 ;@requires R2 ;@ensures E2 ;@*/It assumes from the pre-state the condition:P1 && P2 && ((A1 && R1 ) || (A2 && R2 ))and guarantees that the following condition holds in post-state:Q1 && Q2 &&(\old(A1 && R1 ) ==> E1 ) && (\old(A2 && R2 ) ==> E2 )Here is now an ACSL specification:12/*@ requires P1 ;@ requires P2 ;88A.2.
COMPARISON WITH JML@ ensures Q1 ;@ ensures Q2 ;@ behavior x1 :@ assumes A1 ;@requires R1 ;@ensures E1 ;@ behavior x2 :@ assumes A2 ;@requires R2 ;@ensures E2 ;@*/345678910111213Syntactically, the only difference with the JML specification is the addition of the assumesclauses. Its translation to assume-guarantee is however quite different. It assumes from thepre-state the condition:P1 && P2 && (A1 ==> R1 ) && (A2 ==> R2 )and guarantees that the following condition holds in the post-state:Q1 && Q2 && (\old(A1 ) ==> E1 ) && (\old(A2 ) ==> E2 )Thus, ACSL allows to distinguish between the clauses that control which behavior is active(the assumes clauses) and the clauses that are preconditions for a particular behavior (theinternal requires clauses). In addition, as mentioned above, there is by default no requirementin ACSL for the specification to be complete (The last part of the JML condition on the prestate).
If desired, this has to be precised explicitly with a complete behaviors clause as seenin Section 2.3.3.A.2.2Deductive verification vs. RACSugar-free behaviorsAs explained in details in [23], JML heavyweight behaviors can be viewed as syntactic sugar(however complex it is) that can be translated automatically into more basic contracts consisting mostly of pre- and postconditions and frame conditions.
This allows complex nestingof behaviors from the user point of view, while tools only have to deal with basic contracts. Inparticular, the major tools on JML use this desugaring process, like the Common JML toolsto do assertion checking, unit testing, etc. (see [19]) and the tool ESC/Java2 for automaticdeductive verification of JML specifications (see [6]).One issue with such a desugaring approach is the complexity of the transformations involved,as e.g. for desugaring assignable clauses between multiple spec-cases in JML [23]. Anotherissue is precisely that tools only see one global contract, instead of multiple independentbehaviors, that could be analyzed separately in more detail.
Instead, we favor the view thata function implements multiple behaviors, that can be analyzed separately if a tool feels likeit. Therefore, we do not intend to provide a desugaring process.Axiomatized functions in specificationsJML only allows pure Java methods to be called in specifications [17]. This is certainlyunderstandable when relying on RAC: methods called should be defined so that the runtimecan call them, and they should not have side-effects in order not to pollute the program theyare supposed to annotate.89APPENDIX A.
APPENDICESIn our setting, it is desirable to allow calls to logical functions in specifications. These functions may be defined, like program ones, but they may also be only declared (with a suitabledeclaration of reads clause) and defined through an axiomatization. This makes for richerspecifications that may be useful either in automatic or in manual deductive verification.A.2.3Syntactic differencesThe following table summarizes the difference between JML keywords and ACSL ones, whenthe intent is the same, although minor differences might exist.A.3JMLmodifiable,assignablemeasured_byloop_invariantdecreasesACSLassignsdecreasesloop invariantloop variant( \forall τ x ; P ; Q)( \exists τ x ; P ; Q)\max τ x ; a <= x <= b ; f)( \forall τ x ; P ==> Q)( \exists τ x ; P && Q)\max(a,b,\lambda τ x ; f)Typing rulesDisclaimer: this section is unfinished, it is left here just to give an idea of what it will looklike in the final document.A.3.1Rules for termsInteger promotion:Γ`e:τΓ ` e : integerif τ is any C integer type char, short, int, or long, whatever attribute they have, inparticular signed or unsignedVariables:Γ ` id : τif id : τ ∈ ΓUnary integer operations:Γ ` t : integerif op ∈ {+, −, ∼}Γ ` op t : integerBoolean negation:Γ ` t : booleanΓ `! t : booleanPointer dereferencing:Γ ` t : τ∗Γ ` ∗t : τAddress operator:Γ`t:τΓ ` &t : τ ∗90A.4.
SPECIFICATION TEMPLATESBinaryΓ ` t1 : integerΓ ` t2 : integerif op ∈ {+, −, ∗, /, %}Γ ` t1 op t2 : integerΓ ` t1 : realΓ ` t2 : realif op ∈ {+, −, ∗, /}Γ ` t1 op t2 : realΓ ` t1 : integerΓ ` t2 : integerif op ∈ {==, ! =, <=, <, >=, >}Γ ` t1 op t2 : booleanΓ ` t1 : realΓ ` t2 : realif op ∈ {==, ! =, <=, <, >=, >}Γ ` t1 op t2 : booleanΓ ` t1 : τ ∗Γ ` t2 : τ ∗if op ∈ {==, ! =, <=, <, >=, >}Γ ` t1 op t2 : boolean(to be continued)A.3.2Typing rules for setsWe consider the typing judgement Γ, Λ ` s : τ, b meaning that s is a set of terms of type τ ,which is moreover a set of locations if the boolean b is true. Γ is the C environment and Λis the logic environment.Rules:Γ, Λ ` id : τ, trueΓ, Λ ` id : τ, trueif id : τ ∈ Γif id : τ ∈ ΛΓ, Λ ` s : τ ∗, bΓ, Λ ` ∗s : τ, trueid : τ s : set < struct S∗ >` s− > id : set < τ >Γ, b ∪ Λ ` e : tsetτΓ, Λ ` {e | b; P } : tsetτΓ, Λ ` e1 : τ, b Γ, Λ ` e2 : τ, bΓ, Λ ` e1 , e2 : τ, bA.4Specification TemplatesThis section describes some common issues that may occur when writing an ACSL specification and proposes some solution to overcome themA.4.1Accessing a C variable that is maskedThe situation may happen where it is necessary to refer in an annotation to a C variablethat is masked at that point.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
