зеркало из https://github.com/microsoft/ivy.git
18 строки
181 B
Plaintext
18 строки
181 B
Plaintext
|
#lang ivy1.7
|
||
|
|
|
||
|
|
var p : bool
|
||
|
|
var q : bool
|
||
|
|
|
||
|
|
action a = {
|
||
|
|
assume p & ~q;
|
||
|
|
if p | q {
|
||
|
|
assert false
|
||
|
|
}
|
||
|
|
else {
|
||
|
|
assert false
|
||
|
|
};
|
||
|
|
p := true;
|
||
|
|
}
|
||
|
|
|
||
|
|
export a
|