diff options
author | qunyanm <unknown> | 2016-03-28 14:51:00 -0700 |
---|---|---|
committer | qunyanm <unknown> | 2016-03-28 14:51:00 -0700 |
commit | 62eb04905d6dcb3ab0b6d7cbf1051c97fec01474 (patch) | |
tree | 002242ed44f718fc916ac83643ffdc5682260b3d /Source/Dafny/Translator.cs | |
parent | 91cee1c2028f9ad995df863f2a4568d95f4ea1a8 (diff) |
Allow users to annontate a method as main with {:main} attribute. It’s an error
if more than one method is so annotated. For that method, the usual restrictions
for "main" apply, but it is allowed to take ghost arguments, and it is allowed
to have preconditions. This lets the programmer add some explicit assumptions
about the outside world, modeled, for example, via ghost parameters.
Diffstat (limited to 'Source/Dafny/Translator.cs')
0 files changed, 0 insertions, 0 deletions