Chalice/tests/general-tests/FunctionPostcondition.chalice


1
2
3
4
5
6
7
8
9
10

// this test is for function postconditions

class FunctionPostconditions
{
  predicate valid { true }
  
  function t1(): int
    ensures unfolding valid in true;
  { 1 }
}