ACSL Language Reference (811287), страница 16
Текст из файла (страница 16)
Not only the language features87APPENDIX A. APPENDICESare not the same but the programming styles and idioms are very different, whichentails also different ways of specifying behaviors. In particular, C has no inheritancenor exceptions, and no language support for the simplest properties on memory (e.g,the size of an allocated memory block).• JML relies on runtime assertion checking (RAC) when typing, static analysis and automatic deductive verification fail. The example of CCured [21, 7], that adds strongtyping to C by relying on RAC too, shows that it is not possible to do it in a modularway.
Indeed, it is necessary to modify the layout of C data structures for RAC, whichis not modular. The follow-up project Deputy [8] thus reduces the checking power ofannotations in order to preserve modularity. On the contrary, we choose not to restrainthe power of annotations (e.g., all first order logic formulas are allowed). To that end,we rely on manual deductive verification using an interactive theorem prover (e.g., Coq)when every other technique failed.In the remainder of this chapter, we describe these differences in further details.A.2.1Low-level language vs.
inheritance-based oneNo inherited specificationsJML has a core notion of inheritance of specifications, that duplicates in specifications theinheritance feature of Java. 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.”88A.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:89APPENDIX 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 ;90A.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 [22], 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.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
