ivy/test/mc2.ivy

18 строки
122 B
XML

#lang ivy1.7
type t = {f,g,h}
var x : t
invariant x = f
after init {
x := f
}
action a = {
x := g
}
export a