Commit 883ccddf by Piotr Trojanek Committed by Pierre-Marie de Rodat

[Ada] Fix inconsistent documentation for the Contract_Cases pragma

This patch propagates the renaming from "condition" to "case guard" in the
contract grammar to the paragraphs that describe the pragma semantics.

2018-05-24  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* doc/gnat_rm/implementation_defined_pragmas.rst (Contract_Cases):
	Change "condition" to "case guard" after renaming in the contract
	grammar.
	* gnat_rm.texi: Regenerate.

From-SVN: r260647
parent ebea257e
2018-05-24 Piotr Trojanek <trojanek@adacore.com>
* doc/gnat_rm/implementation_defined_pragmas.rst (Contract_Cases):
Change "condition" to "case guard" after renaming in the contract
grammar.
* gnat_rm.texi: Regenerate.
2018-05-24 Hristian Kirtchev <kirtchev@adacore.com>
* exp_util.adb (Expand_Static_Predicates_In_Choices): Indicate that the
......
......@@ -1173,9 +1173,9 @@ are equivalent to
pragma Postcondition (if C2 then Pred2);
The precondition ensures that one and only one of the conditions is
The precondition ensures that one and only one of the case guards is
satisfied on entry to the subprogram.
The postcondition ensures that for the condition that was True on entry,
The postcondition ensures that for the case guard that was True on entry,
the corrresponding consequence is True on exit. Other consequence expressions
are not evaluated.
......@@ -1190,13 +1190,13 @@ expressed as contract cases:
The placement and visibility rules for ``Contract_Cases`` pragmas are
identical to those described for preconditions and postconditions.
The compiler checks that boolean expressions given in conditions and
consequences are valid, where the rules for conditions are the same as
The compiler checks that boolean expressions given in case guards and
consequences are valid, where the rules for case guards are the same as
the rule for an expression in ``Precondition`` and the rules for
consequences are the same as the rule for an expression in
``Postcondition``. In particular, attributes ``'Old`` and
``'Result`` can only be used within consequence expressions.
The condition for the last contract case may be ``others``, to denote
The case guard for the last contract case may be ``others``, to denote
any case not captured by the previous cases. The
following is an example of use within a package spec:
......@@ -1214,7 +1214,7 @@ following is an example of use within a package spec:
The meaning of contract cases is that only one case should apply at each
call, as determined by the corresponding condition evaluating to True,
call, as determined by the corresponding case guard evaluating to True,
and that the consequence for this case should hold when the subprogram
returns.
......
......@@ -21,7 +21,7 @@
@copying
@quotation
GNAT Reference Manual , Apr 23, 2018
GNAT Reference Manual , Apr 24, 2018
AdaCore
......@@ -2556,9 +2556,9 @@ pragma Postcondition (if C1 then Pred1);
pragma Postcondition (if C2 then Pred2);
@end example
The precondition ensures that one and only one of the conditions is
The precondition ensures that one and only one of the case guards is
satisfied on entry to the subprogram.
The postcondition ensures that for the condition that was True on entry,
The postcondition ensures that for the case guard that was True on entry,
the corrresponding consequence is True on exit. Other consequence expressions
are not evaluated.
......@@ -2572,13 +2572,13 @@ pragma Contract_Cases (P => Q);
The placement and visibility rules for @code{Contract_Cases} pragmas are
identical to those described for preconditions and postconditions.
The compiler checks that boolean expressions given in conditions and
consequences are valid, where the rules for conditions are the same as
The compiler checks that boolean expressions given in case guards and
consequences are valid, where the rules for case guards are the same as
the rule for an expression in @code{Precondition} and the rules for
consequences are the same as the rule for an expression in
@code{Postcondition}. In particular, attributes @code{'Old} and
@code{'Result} can only be used within consequence expressions.
The condition for the last contract case may be @code{others}, to denote
The case guard for the last contract case may be @code{others}, to denote
any case not captured by the previous cases. The
following is an example of use within a package spec:
......@@ -2594,7 +2594,7 @@ end Math_Functions;
@end example
The meaning of contract cases is that only one case should apply at each
call, as determined by the corresponding condition evaluating to True,
call, as determined by the corresponding case guard evaluating to True,
and that the consequence for this case should hold when the subprogram
returns.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment