Changes between Version 42 and Version 43 of Language

Timestamp:

05/21/23 22:02:09 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -793 +793 @@
 == Contract Annotations #contracts
 
-clauses
+Function contracts can be specified as annotations---formatted comments---preceding a function prototype or definition.
+The language for these annotations is based on the specification language [https://frama-c.com/html/acsl.html ACSL] used by Frama-C.
+The high-level syntax is
+
+  `/*@` ''clause''* `*/`
+
+Optionally, any line after the first line (which begins with `/*@` in the contract may have `*` as its first non-white-space character;
+this character is ignored.
+
+There are clauses for preconditions, postconditions, and other concepts.
+These are used in various experimental extensions of CIVL.
+Here me describe the two clauses which are fully supported and in effect by the CIVL model checker.
+
+=== Specifying a guard: `enabled_when`
+
+This clause has syntax
+  `enabled_when` ''expr'' `;`
+It may be used with an [#atomic_f atomic] or [#system system] function.
+This clause specifies a guard that applies whenever the function is called.
+The ''expr'' may use the formal parameters of the functions as well as any other variables that are in scope.
+Whenever control in a process is at a call to the function, the call will be enabled only if the guard evaluates to ''true''.
+The actual arguments used in the call are substituted for the formal parameters in the guard expression.
+
+Note: if the actual arguments have side-effects, they are automatically refactored so that the side-effects occur once, before the call.
+I.e., the call
+  ''f''`(`''expr,,1,,''`,` ''expr,,2,,''`,` ...`)`
+is semantically equivalent to
+  `t1 =` ''expr,,1,,''`;`
+
+  `t2 =` ''expr,,2,,''`;`
+
+  ...
+
+  ''f''`(t1, t2,` ... `)`
+
+Hence the guard may be evaluated any number of times without causing additional side-effects.
+
 
 === The `depends_on` clause #depends_on