|
#lang ivy1.6
|
|
|
|
|
|
action foo(inp:bool)
|
|
|
|
object spec = {
|
|
before foo {
|
|
assert inp
|
|
}
|
|
}
|
|
|
|
object impl = {
|
|
|
|
individual thing : bool
|
|
|
|
object bar = {
|
|
|
|
object spec = {
|
|
after foo {
|
|
assert thing
|
|
}
|
|
}
|
|
|
|
object impl = {
|
|
implement foo {
|
|
thing := inp
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
|
|
export foo
|
|
|
|
isolate iso_this = this
|