diff options
author | kyessenov <unknown> | 2010-07-03 06:43:54 +0000 |
---|---|---|
committer | kyessenov <unknown> | 2010-07-03 06:43:54 +0000 |
commit | 1dcc94a829b160dfce1debc14d07387d0edc85d0 (patch) | |
tree | eb96feb3ac8f94aabfae3417a9d949f90719527a /Test/dafny0/Array.dfy | |
parent | ea0e6d0776c219acbd4af0345038f89bd49bc328 (diff) |
Dafny: added assertions in the refinement obligation necessitating that the return values of concrete and abstract executions are equal. Refactored a test to simulate "static" function call.
Diffstat (limited to 'Test/dafny0/Array.dfy')
0 files changed, 0 insertions, 0 deletions