// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module A {
class C {
var x: int;
protected predicate Valid()
reads this;
{
0 <= x
}
protected function Get(): int
reads this;
{
x
}
constructor ()
modifies this;
ensures Valid();
{
x := 8;
}
method M()
requires Valid();
{
assert Get() == x;
assert x == 8; // error
}
}
}
module A' refines A {
class C {
protected predicate Valid...
{
x == 8
}
method N()
requires Valid();
{
assert Get() == x;
assert x == 8;
}
}
}
module B {
import X as A
method Main() {
var c := new X.C();
c.M(); // fine
c.x := c.x + 1;
c.M(); // error, because Valid() is opaque
}
method L(c: X.C)
requires c != null;
modifies c;
{
assert c.Get() == c.x; // error because Get() is opaque
if * {
assert c.Valid(); // error, because Valid() is opaque
} else if * {
c.x := 7;
assert c.Valid(); // error, because Valid() is opaque
} else {
c.x := 8;
assert c.Valid(); // error, because Valid() is opaque
}
}
}
module B_direct {
import X as A'
method Main() {
var c := new X.C();
c.M(); // fine
c.x := c.x + 1;
if * {
assert c.Valid(); // error, because Valid() is opaque
} else {
c.M(); // error, because Valid() is opaque
}
}
method L(c: X.C)
requires c != null;
modifies c;
{
assert c.Get() == c.x; // error because Get() s opaque
if * {
assert c.Valid(); // error, because Valid() is opaque
} else if * {
c.x := 7;
assert c.Valid(); // error, because Valid() is opaque
} else {
c.x := 8;
assert c.Valid(); // error, because Valid() is opaque
}
}
}
module B' refines B {
import X = A' // this by itself produces no more error
method Main'() {
var c := new X.C();
c.M(); // fine
c.x := c.x + 1;
if * {
assert c.Valid(); // error, because Valid() is opaque
} else {
c.M(); // error, because Valid() is opaque
}
}
method L'(c: X.C)
requires c != null;
modifies c;
{
assert c.Get() == c.x; // error because Get() s opaque
if * {
assert c.Valid(); // error, because Valid() is opaque
} else if * {
c.x := 7;
assert c.Valid(); // error, because Valid() is opaque
} else {
c.x := 8;
assert c.Valid(); // error, because Valid() is opaque
}
}
}
// ---------------------------------
module OpaqueFunctionsAreNotInlined {
predicate {:opaque} F(n: int)
{
0 <= n < 100
}
method M()
{
var x := 18;
assert F(x); // error: cannot be determined, since F is opaque
}
method M'()
{
var x := 18;
reveal_F();
assert F(x);
}
}
// --------------------------------- opaque and refinement
module M0 {
function {:opaque} F(): int
{ 12 }
}
module M1 refines M0 {
}
// ---------------------------------- opaque and generics
function{:opaque} id(x : A):A { x }
method id_ok()
{
reveal_id();
assert id(1) == 1;
}
method id_fail()
{
assert id(1) == 1;
}
datatype Box = Bx(A)
function{:opaque} id_box(x : Box):Box { x }
method box_ok()
{
reveal_id();
assert id(Bx(1)) == Bx(1);
}
method box_fail()
{
assert id(Bx(1)) == Bx(1);
}
// ------------------------- opaque and layer quantifiers
module LayerQuantifiers
{
function{:opaque} f(x:nat) : bool { if x == 0 then true else f(x-1) }
method rec_should_ok()
{
reveal_f();
assert f(1);
}
method rec_should_fail()
{
assert f(1);
}
method rec_should_unroll_ok(one : int)
requires one == 1;
{
reveal_f();
// this one should have enough fuel
assert f(one + one);
}
method rec_should_unroll_fail(one : int)
requires one == 1;
{
reveal_f();
// this one does not have enough fuel
assert f(one + one + one);
}
}
// ------------------------------------- regression test
module Regression
{
datatype List = Nil | Cons(A, tl: List)
function Empty(): List { Nil }
function {:opaque} Length(s: List): int
ensures 0 <= Length(s)
{
if s.Cons? then 1 + Length(s.tl) else 0
}
lemma Empty_ToZero()
ensures Length(Empty()) == 0; // this line once caused the verifier to crash
{
reveal_Length();
}
}