Skip to content

update contracts.dd to reflect DIP1009 #2339

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
wilzbach merged 2 commits into from
Jul 17, 2018
Merged

update contracts.dd to reflect DIP1009 #2339

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
45e12d5
update contracts.dd to reflect DIP1009
zachthemystic Apr 10, 2018
6c5b4f1
split up function grammar to pass pdf gen
Jul 17, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion spec/class.dd
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -868,8 +868,9 @@ $(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) ;)
)

$(P $(I ClassInvariant) specify the relationships among the members of a class instance.
Expand Down
134 changes: 83 additions & 51 deletions spec/contracts.dd
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -61,82 +63,104 @@ $(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
Copy link
Contributor

@wilzbach wilzbach Jul 16, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure about this, but I would spell them pre-contracts and post-contracts? (Google even suggest precontract)

Copy link
Contributor Author

@zachthemystic zachthemystic Jul 16, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just copied the style of the previous documentation. It seems subjective, and not a source of confusion.

come at the end of the function signature and before the opening brace of the function body.)

$(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:)
------
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 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 `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 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
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)
Copy link
Contributor

@wilzbach wilzbach Jul 16, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FWIW D/Phobos style is to indent on the same level: https://dlang.org/dstyle.html#phobos_declarations

{
// 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 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.)

$(H2 $(LNAME2 in_out_inheritance, In, Out and Inheritance))

$(P If a function in a derived class overrides a function from its
Expand Down Expand Up @@ -184,11 +208,21 @@ 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
`AssertError`s when they fail. Since DMD version 2.081.0,
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
Expand Down Expand Up @@ -249,9 +283,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.)

Expand Down
7 changes: 5 additions & 2 deletions spec/expression.dd
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
94 changes: 85 additions & 9 deletions spec/function.dd
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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))
Expand Down Expand Up @@ -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)
Expand All @@ -75,30 +83,98 @@ $(GNAME MemberFunctionAttribute):
$(GLINK FunctionAttribute)
)

$(H3 Function body)

$(GRAMMAR
$(GNAME FunctionBody):
$(GLINK2 statement, BlockStatement)
$(GLINK FunctionContracts)$(OPT) $(GLINK BodyStatement)
$(GLINK FunctionContracts)
$(GLINK SpecifiedFunctionBody)
$(GLINK MissingFunctionBody)
<<<<<<< HEAD

$(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)
=======
)
>>>>>>> 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)
Copy link
Contributor

@wilzbach wilzbach Jul 16, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't there a semi-colon missing?

Copy link
Contributor Author

@zachthemystic zachthemystic Jul 16, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No. The existing grammar is peculiar, and possibly bad design, but it is meant to prevent a semicolon coming after the end brace, };, as in:

int func() in { ... }; // <-- bad, already an error

The way you indicate the body here would be to now say do. Anything else (other than another in or out) means the function body is missing, and the declaration is over, and the parser moves on.

Arguably the no-semicolon-after-brace design is questionable. It hasn't ever mattered much, because currently a contact without a body is only legal in interface declarations, and rarely appears. It could however be expanded to ordinary function declarations eventually, at which point we might see more complaints about it. (e.g. "Why can't I just add the semicolon?")

Anyway, after a parenthesized contract with no body, the expectation would be for the semicolon to be there:

int func() in(...); // <-- legal and expected

Copy link
Contributor

@wilzbach wilzbach Jul 16, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks a lot for the extensive explanation.
For the record, I do think this will be confusing for users if contracts are ever allowed for declaration-only functions/structs/classes:

int func() in(...);  // required
int func() in(...); // error

But yeah that's DMD's current behaviour: https://run.dlang.io/is/UwxsE0

)

$(H3 Function contracts)

$(GRAMMAR
$(GNAME FunctionContracts):
$(GLINK InStatement) $(GLINK OutStatement)$(OPT)
$(GLINK OutStatement) $(GLINK InStatement)$(OPT)
$(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))

$(GNAME InStatement):
$(D in) $(GLINK2 statement, BlockStatement)

$(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
Expand Down
3 changes: 2 additions & 1 deletion spec/struct.dd
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1227,8 +1227,9 @@ $(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) ;)
)

$(P $(I StructInvariant)s specify the relationships among the members of a struct instance.
Expand Down