davidcok
commented
6 years ago I corrected per the comments and merged.
- David
On Mar 6, 2018, at 10:04 AM, Virgile Prevosto notifications@github.com wrote:
@vprevosto commented on this pull request.
OK modulo remarks above.
In compjml_modern.tex https://github.com/acsl-language/acsl/pull/31#discussion_r172445697:
@@ -183,12 +183,16 @@ \subsubsection*{C contracts are not Java ones}
This is equivalent to the previous requirement, except here behaviors can be completed with postconditions that belong to one behavior only. -Contrary to JML, the set of behaviors for a function do not + +\subsubsection*{ACSL contracts vs. JML ones} + +In JML, the set of stated behaviors is assumed to cover all +permitted uses of the function; any calling context in which none of the preconditions are true would be identified as an error. Would it be possible to use another term than "preconditions" here? In ACSL, we tend to reserve that for requires clauses, while the assumes clauses that govern the activation of a behavior would be referred to as "assumptions" or "hypotheses".
In compjml_modern.tex https://github.com/acsl-language/acsl/pull/31#discussion_r172446838:
@@ -261,45 +254,65 @@ \subsubsection*{ACSL contracts vs. JML ones}
\noindent Syntactically, the only difference with the JML specification is the -addition of the \lstinline|assumes| clauses. -Its translation to assume-guarantee is however quite different. -It assumes from the pre-state the condition: +addition of the \lstinline|assumes| clauses and allowing an +anonymous behavior at the beginning of the contract. Rewriting the anonymous behavior with a name gives + +\begin{listing}{1}
- /*@
- @ behavior $x_0$:
- @ assumes true; this should read \true (technically, if you #include
, you could use the C standard macro true here, and that would be desugared onto something like 1 != 0, but in ACSL the proper always-true predicate is \true) In compjml_modern.tex https://github.com/acsl-language/acsl/pull/31#discussion_r172446975:
\begin{listing-nonumber}
- $P_1$ && $P_2$ && ($A_1$ ==> $R_1$) && ($A_2$ ==> $R_2$)
- (true ==> ($P_1$ && $P_2$)) && ($A_1$ ==> $R_1$) && ($A_2$ ==> $R_2$) I'd probably go for \true here as well.
In compjml_modern.tex https://github.com/acsl-language/acsl/pull/31#discussion_r172448593:
This makes for richer specifications that may be useful either in automatic or in manual deductive verification. +\marginpar{Say something about the intent to allow pure C functions in specifications?} This has been discussed in the context of ACSL++ (where you'd really prefer to avoid writing getters both in the code and in the logic), but it also makes sense to add it to ACSL. An issue can be opened.
— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/31#pullrequestreview-101459895, or mute the thread https://github.com/notifications/unsubscribe-auth/AFExwD0vqBNHPAscmc3un7mysFzQj2k0ks5tblE4gaJpZM4SZyV8.
Updates and corrections and explanations to material about JML