You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The second line would be read "0 <= x" implies "x == y". Implies is a boolean operator with lower precedence than && or ||; it is used in postconditions ("ensures") to make claims that are conditioned on other things. This allows more flexible preconditions and postconditions, without requiring the coder to enter the main body of a function and write traditional conditional expressions before stating the pre/postconditions.
The text was updated successfully, but these errors were encountered:
Consider this snippet of dafny code from http://rise4fun.com/Dafny/tutorial/guide:
The second line would be read "0 <= x" implies "x == y". Implies is a boolean operator with lower precedence than && or ||; it is used in postconditions ("ensures") to make claims that are conditioned on other things. This allows more flexible preconditions and postconditions, without requiring the coder to enter the main body of a function and write traditional conditional expressions before stating the pre/postconditions.
The text was updated successfully, but these errors were encountered: