diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-13 17:44:45 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-13 17:44:45 -0700 |
| commit | 3d56fc351f6a71d90e72ef115477d1be663cfba5 (patch) | |
| tree | c0dbc350b8447b199e3233ba86dea7329553984c /Test/vstte2012 | |
| parent | b2eb7236b06ea3102b8cf86fc8f41c555a089614 (diff) | |
Dafny: Changed the semantics of the assign-such-that statement "x :| P;" to check the existence of a value. The previous "assume only" version is available by supplying the keyword "assume" in front of "P".
Diffstat (limited to 'Test/vstte2012')
0 files changed, 0 insertions, 0 deletions