Test/dafny0/snapshots/Inputs/Snapshots8.v0.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

method M(x: int)
{                     assert x < 20 || 10 <= x;  // always true
  assert x < 10;  // error
  Other(x);  // error: precondition violation
}

method Other(y: int)
  requires 0 <= y
{
}

method Posty() returns (z: int)
  ensures 2 <= z  // error: postcondition violation
{
  var t := 20;
  if t < z {
  } else {  // the postcondition violation occurs on this 'else' branch
  }
}

method NoChangeWhazzoeva(u: int)
{
  assert u != 53;  // error
}

method NoChangeAndCorrect()
{
  assert true;
}