Open
Description
Summary
If you have a specification { after init { ... } } containing assertions and also an implementation { after init { ... } } containing actions, you can assert false in the specification { after init { ... } } if the other assertions in specification { after init { ... } } relate to the result of actions in implementation { after init { ... } }.
Steps to reproduce
Put the following in oops.ivy.
#lang ivy1.7
individual x:bool
specification {
after init {
assert x = true;
assert false;
}
}
implementation {
after init {
x := true;
}
}
Check the file with the following command.
$ ivy_check trace=true oops.ivy
- Expected: Line 8
assert false;should fail. - Actual: Whole file passes.
Removing line 7 assert x = true; or removing line 17 x := true; fixes the issue (line 8 assert false; fails). Additionally, moving both the asserts and the actions into a single after init { ... } outside of either specification { ... } and implementation { ... } resolves the issue.
Present in versions
On kenmcmil/ivy@dbe45e7 on macOS Sonoma.
Metadata
Metadata
Assignees
Labels
No labels