Skip to content
Snippets Groups Projects
Commit 8983f808 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

Fixes demo example

parent c8caf91a
No related branches found
No related tags found
1 merge request!141Fixes demo example
Pipeline #42485 passed
...@@ -75,6 +75,13 @@ void job ( int *t , int A) { ...@@ -75,6 +75,13 @@ void job ( int *t , int A) {
and a specification file: and a specification file:
``` ```
module demo :
axiomatic A {
type event = B | C(integer);
predicate P(integer x);
logic integer phi(event e);
}
function f: function f:
contract: contract:
ensures P(phi(C(\result))); ensures P(phi(C(\result)));
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment