From 45e12d5b949e10beeb83fff69cfc9f3f11035060 Mon Sep 17 00:00:00 2001 From: Zach Tollen Date: Tue, 10 Apr 2018 01:38:08 -0400 Subject: [PATCH 1/2] update contracts.dd to reflect DIP1009 --- spec/class.dd | 1 + spec/contracts.dd | 137 ++++++++++++++++++++++++++++----------------- spec/expression.dd | 7 ++- spec/function.dd | 46 ++++++++++++--- spec/struct.dd | 1 + 5 files changed, 130 insertions(+), 62 deletions(-) diff --git a/spec/class.dd b/spec/class.dd index fe8cf54e7a..7df1922ee1 100644 --- a/spec/class.dd +++ b/spec/class.dd @@ -870,6 +870,7 @@ $(GRAMMAR $(GNAME ClassInvariant): $(D invariant ( )) $(GLINK2 statement, BlockStatement) $(D invariant) $(GLINK2 statement, BlockStatement) + $(D invariant $(LPAREN)) $(GLINK2 expression, ContractArguments) $(D $(RPAREN) ;) ) $(P $(I ClassInvariant) specify the relationships among the members of a class instance. diff --git a/spec/contracts.dd b/spec/contracts.dd index d224a49570..f9ad11e3b0 100644 --- a/spec/contracts.dd +++ b/spec/contracts.dd @@ -33,9 +33,11 @@ $(H2 $(LNAME2 assert_contracts, Assert Contract)) $(P The most basic contract is the $(GLINK2 expression, AssertExpression). - An $(B assert) declares an expression that must evaluate to true:) + An $(B assert) declares an expression that must evaluate to true, with an + optional failure string as a second argument:) ------ assert(expression); +assert(expression, "message to display on failure"); ------ $(P As a contract, an $(D assert) represents a guarantee that the code $(I must) uphold. Any failure of this expression represents a logic @@ -61,82 +63,106 @@ $(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:) + In D, pre contracts begin with `in`, and post contracts begin with `out`. They + come at the end of the function signature and before the opening brace of the function body.) + $(P As of the acceptance of + $(LINK2 https://github.com/dlang/DIPs/blob/master/DIPs/accepted/DIP1009.md, DIP1009), + pre and post contracts can be written either in expression form, with + syntaxes similar to $(B assert), or as block statements containing arbitrary + code.) + + $(P The expression form is:) +------ +in(expression) +in(expression, "failure string") +out(identifier; expression) +out(identifier; expression, "failure string") +out(; expression) +out(; expression, "failure string") +{ + ...function body... +} +------ + $(P The block statement form is:) ------ in { ...contract preconditions... } -out (result) +out +{ + ...contract postconditions... +} +out (identifier) { ...contract postconditions... } do { - ...code... + ...function body... } ------ - $(P Since $(LINK2 https://github.com/dlang/DIPs/blob/master/DIPs/accepted/DIP1003.md, DIP1003 has been applied) - the actual function body starts with $(D do). - In the past, $(D body) was used, and could still be encountered in old code bases. - In the long term, $(D body) may be deprecated, but for now it's allowed - as a keyword in this context and as an identifier in the function body, - although $(D do) is preferred.) + $(P The optional identifier in either type of `out` contract is set to the return value + of the function.) $(P By definition, if a pre contract fails, then the function received bad - parameters. An `AssertError` is thrown. If a post contract fails, - then there is a bug in the function. An `AssertError` is thrown.) - - $(P Either the `in` or the `out` clause can be omitted. - If the `out` contract is for a function - body, the given `result` variable is declared and assigned the return - value of the function. For example, let's implement a square root function:) - ------- -long square_root(long x) -in -{ - assert(x >= 0); -} -out (result) -{ - assert(result ^^ 2 <= x && (result + 1) ^^ 2 > x); -} -do -{ - return cast(long)std.math.sqrt(cast(real)x); -} ------- - $(P The `assert`s in the `in` and `out` bodies are called $(I contracts). - Any other D - statement or expression is allowed in the bodies, but it is important + parameters. If a post contract fails, then there is a bug in the function. In either case, + an `assert` statement within the corresponding `in` or `out` block will throw an + `AssertError`.) + + $(P Notice that the keyword `do` can be used to announce the function body. While any number + of pre or post contracts of any form may follow each other, `do` is + required only when the last contract before the body is a block statement. + (Before the acceptance of + $(LINK2 https://github.com/dlang/DIPs/blob/master/DIPs/accepted/DIP1003.md, DIP1003), + the keyword $(D body) was required instead of `do`, and may still be encountered in + old code bases. In the long term, $(D body) may be deprecated, but for now it's allowed both + as a keyword in this context and as an identifier elsewhere, although $(D do) is preferred.) ) + + $(P While any arbitrary D code is allowed in the `in` and `out` contract blocks, + their only function should be to verify incoming and outgoing data. It is important to ensure that the code has no side effects, and that the release version of the code will not depend on any effects of the code. - For a release build of the code, the `in` and `out` code is not + For a release build of the code, `in` and `out` contracts are not inserted.) -$(H3 $(LNAME2 out_without_result, Post Contracts Without a Result Variable)) + $(P Here is an example function in both forms:) - $(P If the function returns `void`, there is no result, and so there can be no - result variable in the `out` clause. An `out` contract can still be useful, - (e.g. to check a global variable or a `ref` parameter was set correctly).) - - $(P Regardless of return type, `out` contracts don't require a result variable:) ------ -void func() -out +int fun(ref int a, int b) + in(a > 0) + in(b >= 0, "b cannot be negative!") + out(r; r > 0, "return must be positive") + out(; a != 0) +{ + // function body +} + +int fun(ref int a, int b) +in { - ...contracts... + assert(a > 0); + assert(b >= 0, "b cannot be negative!"); +} +out(r) +{ + assert(r > 0, "return must be positive"); + assert(a != 0); } do { - ... + // function body } ------ + $(P The two functions are almost semantically identical. The expressions in the + first are lowered to contract blocks that look almost exactly like the second, + except that a separate block is created for each expression in the first, thus + avoiding shadowing variable names.) + $(H2 $(LNAME2 in_out_inheritance, In, Out and Inheritance)) $(P If a function in a derived class overrides a function from its @@ -184,11 +210,22 @@ class Date invariant { assert(1 <= day && day <= 31); - assert(0 <= hour && hour < 24); + assert(0 <= hour && hour < 24, "hour out of bounds"); } } ------ + $(P Invariant blocks should contain `assert` expressions, and should throw + $(D AssertError)s when they fail. As of + $(LINK2 https://github.com/dlang/DIPs/blob/master/DIPs/accepted/DIP1009.md, DIP1009), + invariants can also be written as expression statements, with `assert` implied: + ) + +------ + invariant(1 <= day && day <= 31); + invariant(0 <= hour && hour < 24, "hour out of bounds"); +------ + $(P The invariant is a contract saying that the `assert`s must hold true. The invariant is checked when a class or struct constructor completes, and at the start of the class or struct destructor. For public or exported @@ -249,9 +286,7 @@ assert(mydate); // check that class Date invariant holds assert(&s); // check that struct S invariant holds ------ - $(P Invariants contain assert expressions, and so when they fail, - they throw $(D AssertError)s. - Class invariants are inherited, that is, + $(P Class invariants are inherited, that is, any class invariant is implicitly in addition to the invariants of its base classes.) diff --git a/spec/expression.dd b/spec/expression.dd index 5b7a5e075b..294ac45224 100644 --- a/spec/expression.dd +++ b/spec/expression.dd @@ -1621,8 +1621,11 @@ $(H3 $(LNAME2 assert_expressions, Assert Expressions)) $(GRAMMAR $(GNAME AssertExpression): - $(D assert $(LPAREN)) $(GLINK AssignExpression) $(D ,)$(OPT) $(D $(RPAREN)) - $(D assert $(LPAREN)) $(GLINK AssignExpression) $(D ,) $(GLINK AssignExpression) $(D ,)$(OPT) $(D $(RPAREN)) + $(D assert $(LPAREN)) $(GLINK ContractArguments) $(D $(RPAREN)) + +$(GNAME ContractArguments): + $(GLINK AssignExpression) $(D ,)$(OPT) + $(GLINK AssignExpression) $(D ,) $(GLINK AssignExpression) $(D ,)$(OPT) ) $(P The first $(I AssignExpression) must evaluate to true. If it does not, an $(I Assert Failure) diff --git a/spec/function.dd b/spec/function.dd index 10049e138b..6df10490f9 100644 --- a/spec/function.dd +++ b/spec/function.dd @@ -77,13 +77,44 @@ $(GNAME MemberFunctionAttribute): $(GRAMMAR $(GNAME FunctionBody): - $(GLINK2 statement, BlockStatement) - $(GLINK FunctionContracts)$(OPT) $(GLINK BodyStatement) - $(GLINK FunctionContracts) + $(GLINK SpecifiedFunctionBody) + $(GLINK MissingFunctionBody) + +$(GNAME FunctionLiteralBody): + $(GLINK SpecifiedFunctionBody) + +$(GNAME SpecifiedFunctionBody): + $(D do)$(OPT) $(GLINK2 statement, BlockStatement) + $(GLINK FunctionContracts)$(OPT) $(GLINK InOutExpression) $(D do)$(OPT) $(GLINK2 statement, BlockStatement) + $(GLINK FunctionContracts)$(OPT) $(GLINK InOutStatement) $(D do)$(OPT) $(GLINK2 statement, BlockStatement) + +$(GNAME MissingFunctionBody): + $(D ;) + $(GLINK FunctionContracts)$(OPT) $(GLINK InOutExpression) $(D ;) + $(GLINK FunctionContracts)$(OPT) $(GLINK InOutStatement) $(GNAME FunctionContracts): - $(GLINK InStatement) $(GLINK OutStatement)$(OPT) - $(GLINK OutStatement) $(GLINK InStatement)$(OPT) + $(GLINK FunctionContract) + $(GLINK FunctionContract) $(I FunctionContracts) + +$(GNAME FunctionContract): + $(GLINK InOutExpression) + $(GLINK InOutStatement) + +$(GNAME InOutExpression): + $(GLINK InExpression) + $(GLINK OutExpression) + +$(GNAME InOutStatement): + $(GLINK InStatement) + $(GLINK OutStatement) + +$(GNAME InExpression): + $(D in $(LPAREN)) $(GLINK2 expression, ContractArguments) $(D $(RPAREN)) + +$(GNAME OutExpression): + $(D out $(LPAREN) ;) $(GLINK2 expression, ContractArguments) $(D $(RPAREN)) + $(D out $(LPAREN)) $(I Identifier) $(D ;) $(GLINK2 expression, ContractArguments) $(D $(RPAREN)) $(GNAME InStatement): $(D in) $(GLINK2 statement, BlockStatement) @@ -91,14 +122,11 @@ $(GNAME InStatement): $(GNAME OutStatement): $(D out) $(GLINK2 statement, BlockStatement) $(D out) $(D $(LPAREN)) $(I Identifier) $(D $(RPAREN)) $(GLINK2 statement, BlockStatement) - -$(GNAME BodyStatement): - $(D body) $(GLINK2 statement, BlockStatement) ) $(H2 $(LNAME2 contracts, Contracts)) - $(P The $(D in) and $(D out) blocks of a function declaration specify + $(P The $(D in) and $(D out) blocks or expressions of a function declaration specify the pre- and post-conditions of the function. They are used in $(LINK2 contracts.html, Contract Programming). The code inside these blocks should diff --git a/spec/struct.dd b/spec/struct.dd index b2ae6bed75..13ae9e64fd 100644 --- a/spec/struct.dd +++ b/spec/struct.dd @@ -1229,6 +1229,7 @@ $(GRAMMAR $(GNAME StructInvariant): $(D invariant ( )) $(GLINK2 statement, BlockStatement) $(D invariant) $(GLINK2 statement, BlockStatement) + $(D invariant $(LPAREN)) $(GLINK2 expression, ContractArguments) $(D $(RPAREN) ;) ) $(P $(I StructInvariant)s specify the relationships among the members of a struct instance. From 6c5b4f1f6af85d4cd20550d72635abbfcd66dace Mon Sep 17 00:00:00 2001 From: Zach Tollen Date: Mon, 16 Jul 2018 23:30:49 -0400 Subject: [PATCH 2/2] split up function grammar to pass pdf gen --- spec/class.dd | 2 +- spec/contracts.dd | 23 ++++++++++------------- spec/function.dd | 48 +++++++++++++++++++++++++++++++++++++++++++++++ spec/struct.dd | 2 +- 4 files changed, 60 insertions(+), 15 deletions(-) diff --git a/spec/class.dd b/spec/class.dd index 7df1922ee1..f29407c0d6 100644 --- a/spec/class.dd +++ b/spec/class.dd @@ -868,7 +868,7 @@ $(H2 $(LNAME2 invariants, Class Invariants)) $(GRAMMAR $(GNAME ClassInvariant): - $(D invariant ( )) $(GLINK2 statement, BlockStatement) + $(D invariant $(LPAREN) $(RPAREN)) $(GLINK2 statement, BlockStatement) $(D invariant) $(GLINK2 statement, BlockStatement) $(D invariant $(LPAREN)) $(GLINK2 expression, ContractArguments) $(D $(RPAREN) ;) ) diff --git a/spec/contracts.dd b/spec/contracts.dd index f9ad11e3b0..f1e3265ce4 100644 --- a/spec/contracts.dd +++ b/spec/contracts.dd @@ -66,11 +66,9 @@ $(H2 $(LNAME2 pre_post_contracts, Pre and Post Contracts)) In D, pre contracts begin with `in`, and post contracts begin with `out`. They come at the end of the function signature and before the opening brace of the function body.) - $(P As of the acceptance of - $(LINK2 https://github.com/dlang/DIPs/blob/master/DIPs/accepted/DIP1009.md, DIP1009), - pre and post contracts can be written either in expression form, with - syntaxes similar to $(B assert), or as block statements containing arbitrary - code.) + $(P Pre and post contracts can be written either in expression form (feature introduced in DMD + 2.081.0), with a syntax similar to $(B assert), or as block statements + containing arbitrary code.) $(P The expression form is:) ------ @@ -112,16 +110,16 @@ do an `assert` statement within the corresponding `in` or `out` block will throw an `AssertError`.) - $(P Notice that the keyword `do` can be used to announce the function body. While any number + $(P The keyword `do` can be used to announce the function body. Although any number of pre or post contracts of any form may follow each other, `do` is required only when the last contract before the body is a block statement. (Before the acceptance of $(LINK2 https://github.com/dlang/DIPs/blob/master/DIPs/accepted/DIP1003.md, DIP1003), - the keyword $(D body) was required instead of `do`, and may still be encountered in - old code bases. In the long term, $(D body) may be deprecated, but for now it's allowed both - as a keyword in this context and as an identifier elsewhere, although $(D do) is preferred.) ) + the keyword `body` was required instead of `do`, and may still be encountered in + old code bases. In the long term, `body` may be deprecated, but for now it's allowed both + as a keyword in this context and as an identifier elsewhere, although `do` is preferred.) ) - $(P While any arbitrary D code is allowed in the `in` and `out` contract blocks, + $(P Though any arbitrary D code is allowed in the `in` and `out` contract blocks, their only function should be to verify incoming and outgoing data. It is important to ensure that the code has no side effects, and that the release version of the code @@ -158,7 +156,7 @@ do } ------ - $(P The two functions are almost semantically identical. The expressions in the + $(P The two functions are almost identical semantically. The expressions in the first are lowered to contract blocks that look almost exactly like the second, except that a separate block is created for each expression in the first, thus avoiding shadowing variable names.) @@ -216,8 +214,7 @@ class Date ------ $(P Invariant blocks should contain `assert` expressions, and should throw - $(D AssertError)s when they fail. As of - $(LINK2 https://github.com/dlang/DIPs/blob/master/DIPs/accepted/DIP1009.md, DIP1009), + `AssertError`s when they fail. Since DMD version 2.081.0, invariants can also be written as expression statements, with `assert` implied: ) diff --git a/spec/function.dd b/spec/function.dd index 6df10490f9..b5d95f5358 100644 --- a/spec/function.dd +++ b/spec/function.dd @@ -6,6 +6,8 @@ $(HEADERNAV_TOC) $(H2 $(LNAME2 grammar, Grammar)) +$(H3 Function declaration) + $(GRAMMAR $(GNAME FuncDeclaration): $(GLINK2 declaration, StorageClasses)$(OPT) $(GLINK2 declaration, BasicType) $(GLINK FuncDeclarator) $(GLINK FunctionBody) @@ -22,6 +24,8 @@ $(GNAME FuncDeclaratorSuffix): $(GLINK2 template, TemplateParameters) $(GLINK Parameters) $(GLINK MemberFunctionAttributes)$(OPT) $(GLINK2 template, Constraint)$(OPT) ) +$(H3 Parameters) + $(GRAMMAR $(GNAME Parameters): $(D $(LPAREN)) $(GLINK ParameterList)$(OPT) $(D $(RPAREN)) @@ -52,7 +56,11 @@ $(GNAME InOutX): $(D ref) $(RELATIVE_LINK2 return-ref-parameters, $(D return ref)) $(D scope) +) + +$(H3 Function attributes) +$(GRAMMAR $(GNAME FunctionAttributes): $(GLINK FunctionAttribute) $(GLINK FunctionAttribute) $(I FunctionAttributes) @@ -75,10 +83,13 @@ $(GNAME MemberFunctionAttribute): $(GLINK FunctionAttribute) ) +$(H3 Function body) + $(GRAMMAR $(GNAME FunctionBody): $(GLINK SpecifiedFunctionBody) $(GLINK MissingFunctionBody) +<<<<<<< HEAD $(GNAME FunctionLiteralBody): $(GLINK SpecifiedFunctionBody) @@ -92,27 +103,64 @@ $(GNAME MissingFunctionBody): $(D ;) $(GLINK FunctionContracts)$(OPT) $(GLINK InOutExpression) $(D ;) $(GLINK FunctionContracts)$(OPT) $(GLINK InOutStatement) +======= +) +>>>>>>> 0918d24fc7d4515b4e02f1ebf50bf0bf6af32348 + +$(GRAMMAR +$(GNAME FunctionLiteralBody): + $(GLINK SpecifiedFunctionBody) + +$(GNAME SpecifiedFunctionBody): + $(D do)$(OPT) $(GLINK2 statement, BlockStatement) + $(GLINK FunctionContracts)$(OPT) $(GLINK InOutContractExpression) $(D do)$(OPT) $(GLINK2 statement, BlockStatement) + $(GLINK FunctionContracts)$(OPT) $(GLINK InOutStatement) $(D do)$(OPT) $(GLINK2 statement, BlockStatement) + +$(GNAME MissingFunctionBody): + $(D ;) + $(GLINK FunctionContracts)$(OPT) $(GLINK InOutContractExpression) $(D ;) + $(GLINK FunctionContracts)$(OPT) $(GLINK InOutStatement) +) +$(H3 Function contracts) + +$(GRAMMAR $(GNAME FunctionContracts): $(GLINK FunctionContract) $(GLINK FunctionContract) $(I FunctionContracts) $(GNAME FunctionContract): +<<<<<<< HEAD $(GLINK InOutExpression) $(GLINK InOutStatement) $(GNAME InOutExpression): $(GLINK InExpression) $(GLINK OutExpression) +======= + $(GLINK InOutContractExpression) + $(GLINK InOutStatement) + +$(GNAME InOutContractExpression): + $(GLINK InContractExpression) + $(GLINK OutContractExpression) +>>>>>>> 0918d24fc7d4515b4e02f1ebf50bf0bf6af32348 $(GNAME InOutStatement): $(GLINK InStatement) $(GLINK OutStatement) +<<<<<<< HEAD $(GNAME InExpression): $(D in $(LPAREN)) $(GLINK2 expression, ContractArguments) $(D $(RPAREN)) $(GNAME OutExpression): +======= +$(GNAME InContractExpression): + $(D in $(LPAREN)) $(GLINK2 expression, ContractArguments) $(D $(RPAREN)) + +$(GNAME OutContractExpression): +>>>>>>> 0918d24fc7d4515b4e02f1ebf50bf0bf6af32348 $(D out $(LPAREN) ;) $(GLINK2 expression, ContractArguments) $(D $(RPAREN)) $(D out $(LPAREN)) $(I Identifier) $(D ;) $(GLINK2 expression, ContractArguments) $(D $(RPAREN)) diff --git a/spec/struct.dd b/spec/struct.dd index 13ae9e64fd..d5095a816e 100644 --- a/spec/struct.dd +++ b/spec/struct.dd @@ -1227,7 +1227,7 @@ $(H2 $(LNAME2 StructInvariant, Struct Invariants)) $(GRAMMAR $(GNAME StructInvariant): - $(D invariant ( )) $(GLINK2 statement, BlockStatement) + $(D invariant $(LPAREN) $(RPAREN)) $(GLINK2 statement, BlockStatement) $(D invariant) $(GLINK2 statement, BlockStatement) $(D invariant $(LPAREN)) $(GLINK2 expression, ContractArguments) $(D $(RPAREN) ;) )