Skip to content

Commit

Permalink
fix issue 17925 - Mention the old body keyword
Browse files Browse the repository at this point in the history
  • Loading branch information
bbasile authored Nov 20, 2017
1 parent 6e7dd8c commit e6cc783
Showing 1 changed file with 9 additions and 1 deletion.
10 changes: 9 additions & 1 deletion spec/contracts.dd
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ $(H2 $(LNAME2 pre_post_contracts, Pre and Post Contracts))
typical use of this would be in validating the parameters to a function. The post
contracts validate the result of the statement. The most typical use of this
would be in validating the return value of a function and of any side effects it has.
The syntax is:)
The syntax is:

------
in
Expand All @@ -75,6 +75,14 @@ do
...code...
}
------

The actual function body starts with the <code>do</code> keyword.
In the past, <code>body</code> was used and it will be still encountered in old code bases.
On the long term, <code>body</code> could be completely unsupported but for now it's still allowed,
as a keyword in this context and as an identifier in the function body
although <code>do</code> must be prefered.
)

$(P By definition, if a pre contract fails, then the function received bad
parameters.
An AssertError is thrown. If a post contract fails,
Expand Down

0 comments on commit e6cc783

Please sign in to comment.