Add Expression-Based Contract Syntax

Field	Value
DIP:	1009
Review Count:	3
Author:	Zach Tollen(reachzach@gmail.com)
Implementation:	Timon Gehr
Status:	Accepted

Abstract

The D programming language has built-in support for Contract Programming. The in, out and invariant constructs are used to specify preconditions, postconditions and aggregate invariants. Conditions inside contracts are encoded as a sequence of statements that explicitly throws an AssertError exactly in those cases where the condition fails. This is a general way to specify runtime-checkable contracts, but it usually suffices to check that an expression evaluates to true. The present DIP proposes adding shorthand syntax for this use case.

Links

DIP1003 discussion thread.

Rationale

Although D contracts are statements, most contracts are specified as simple Boolean expressions that should evaluate to true. To wit, many programming languages with built-in support for contracts support only Boolean expressions to express contracts. This predominant use case should be supported with a more concise syntax in the D programming language. We expect that the prevalence of function contracts and invariants will increase in response to the improved ergonomics proposed by this DIP.

D code before the proposed change (which will remain valid):

ulong strToDecInt(string s)
in
{
    assert(s.length > 0, "s must not be empty");
}
body
{
    ulong ret = 0;
}

Improved D code after the proposed change:

ulong strToDecInt(string s)
    in(s.length > 0, "s must not be empty");
{
    ulong ret = 0;
}

Description

We propose to introduce, in addition to the current statement-based contract syntax, a short-hand expression-based syntax for in and out contracts as well as invariant contracts. The syntax is designed to mimic that of a call to assert. A few additional considerations are necessary for out contracts, as they require access to the function's return value. (Different options for the out syntax are discussed in the section "new out syntax", where we also motivate our recommended syntax.)

Multiple in and out contracts are permitted for a single function. Expression-based contracts have no terminating semicolons, and the do keyword indicating the beginning of the function body is optional; the body's opening brace is sufficient.

Example:

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
}

Contracts can use either the statement-based syntax or the expression-based syntax. Both may be present in the same function declaration. The do keyword continues to be required as a separator between a statement-based contract and the function body.

Example:

int fun(ref int a, int b)
in(a > 0)
in
{
    assert(b >= 0, "b cannot be negative!");
}
do
{
    // function body
}

For virtual interface functions without a specified function body, a semicolon is required to terminate the function declaration after an expression-based contract specification. (No semicolon is required to terminate such a function declaration after a statement-based contract specification, which is consistent with the current behavior.)

Example:

interface I
{
    int fun(int a) in(a > 0);
}

This DIP also proposes similar syntax for invariant contracts. Like the proposed function contract syntax, the new invariant contract syntax is designed to mimic a call to assert. Expression-based invariant contracts must be terminated with a semicolon. A class or struct definition may contain multiple invariant contracts using either syntactic form.

Example:

class C {
    int data;
    invariant(data != 0, "data cannot be 0");
}

The semantics of the new expression-based contracts is specified by lowering to contracts using the existing statement-based syntax. Expression-based contracts are lowered to statement-based contracts containing a single assert statement with the arguments of the contract.

Example:

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
}

interface I {
    int fun(int a)
        in(a > 0);
}

class C {
    int data;
    invariant(data != 0, "data cannot be 0");
}

Turns into:

int fun(ref int a, int b)
in
{
    assert(a > 0);
}
in
{
    assert(b >= 0, "b cannot be negative!");
}
out(r)
{
    assert(r > 0, "return must be positive");
}
out
{
    assert(a != 0);
}
do
{
    // function body
}

interface I {
    int fun(int a)
    in
    {
        assert(a > 0);
    }
}

class C {
    int data;
    invariant
    {
        assert(data != 0, "data cannot be 0");
    }
}

Multiple statement-based in and out contracts are lowered into single statement-based contracts that execute the statements in the order they appear in the source, but in separated scopes. This is similar to the manner multiple statement-based invariant contracts are already lowered.

Example:

int fun(int x)
in
{
    assert(x > 0);
}
in
{
    assert(x < 10);
}
out(r)
{
    assert(r <1 0);
}
out(s)
{
    assert(s % 2 == 0);
}
out
{
    assert(true);
}
do
{
    // function body
}

Turns into:

int fun(int x)
in
{
    {
        assert(x > 0);
    }
    {
        assert(x < 10);
    }
}
out(__result)
{
    {
        alias r = __result;
        assert(r < 10);
    }
    {
        alias s = __result;
        assert(s % 2 == 0);
    }
}
do
{
    // function body
}

(The implementation can use temporary ref variables instead of alias declarations for better error messages.)

New `out` syntax

Note that our proposed out contract syntax contains a semicolon that is not present in the in contract syntax. This semicolon separates the identifier for the function's return value to be used within the contract condition from the contract condition. The identifier for the return value is optional, but the semicolon is always required. We have considered multiple alternatives before reaching this recommendation:

Require the semicolon only if the return value needs to be bound to an identifier. This leads to ambiguities with the old syntax: out(i) could be parsed as either a contract expression asserting that i is true, or the beginning of an out contract using the old contract syntax that introduces the identifier i for the function's return value.

Example:

int fun(ref int i)
    out(i != 0) // okay
    out(i) // whoops! ambiguous with existing contract syntax
{
   // out contract, not function body
}

Use two sets of parentheses; one to introduce the identifier and one for the contract expression. This is analogous to the statement-based out contract syntax in case the return value needs to be bound (but not otherwise). It also resembles the syntax of template function declarations.

Example:

int fun(ref int i)
    out(r)(r > 0)
    out()(i) // unambiguous with the current contract syntax
{
  // function body
}

(Our recommended solution.) Require the use of a semicolon to separate the contract parameter from the expression body. This resembles the syntax of for and foreach loops, and does not require multiple sets of parentheses. It is also more concise.

Example:

int fun(ref int i)
    out(r; r > 0)
    out(; i > 0)
    out(; i)  // these are all unambiguous
{
    // function body
}

Note that existing foreach statements do not allow omitting the initial identifier, but the proposed syntax does. If more consistency with foreach is desired, we could require that out contracts always introduce an identifier by removing the relevant grammar rule.

Grammar

The grammar for assert arguments is redefined in terms of ContractArguments, which is then used in the grammar rules for all newly-proposed expression-based contract specifications. Existing statement-based in, out and invariant contracts are preserved (with the same semantics). However, in contrast to before, multiple in and out contracts are now allowed on the same function declaration, even if they are statement-based.

Changed grammar rules:

- AssertExpression:
-    assert ( AssignExpression ,[opt] )
-    assert ( AssignExpression , AssignExpression ,[opt] )
+    assert(ContractArguments)

- FunctionContracts:
-     InStatement OutStatement[opt]
-     OutStatement InStatement[opt]
+     FunctionContract
+     FunctionContract FunctionContracts

- FunctionBody:
-     BlockStatement
-     FunctionContracts[opt] BodyStatement
-     FunctionContracts
+     SpecifiedFunctionBody
+     MissingFunctionBody

- FunctionLiteralBody:
-     BlockStatement
-     FunctionContracts[opt] BodyStatement
+     SpecifiedFunctionBody

Invariant:
-     invariant ( ) BlockStatement
-     invariant BlockStatement
+     invariant ( ) BlockStatement
+     invariant BlockStatement
+     invariant ( ContractArguments ) ;

+ ContractArguments:
+     AssignExpression ,[opt]
+     AssignExpression , AssignExpression ,[opt]

+ InContractExpression:
+     in ( ContractArguments )

+ OutContractExpression:
+     out ( ; ContractArguments )
+     out ( Identifier ; ContractArguments )

+ InOutContractExpression:
+     InContractExpression
+     OutContractExpression

+ InOutStatement:
+     InStatement
+     OutStatement

+ FunctionContract:
+     InOutContractExpression
+     InOutStatement

+ SpecifiedFunctionBody:
+     do[opt] BlockStatement
+     FunctionContracts[opt] InOutContractExpression do[opt] BlockStatement
+     FunctionContracts[opt] InOutStatement do BlockStatement

+ MissingFunctionBody:
+     ;
+     FunctionContracts[opt] InOutContractExpression ;
+     FunctionContracts[opt] InOutStatement

Code Breakage

This DIP exclusively proposes additional syntax and thus no code breakage is anticipated.

Acknowledgments

This DIP is based upon an idea initially proposed by H.S. Teoh. It incorporates ideas from Moritz Maxeiner, Solomon E, Timon Gehr, and the DIP author, and was very helpfully edited by Mike Parker and Timon Gehr.

Copyright & License

Licensed under Creative Commons Zero 1.0

Reviews

Preliminary Review Round 1

Reviewed Version

Discussion

The version of the DIP reviewed in this round laid out three requirements for the proposed syntax:

semi-colons must be allowed to terminate contracts in expression form
multiple in/out contracts must be allowed
contracts should be allowed in the function body

During the course of the review, requirements 1 and 2 received negative feedback, the former for being "noisy" and the latter for introducing too much cognitive dissonance. Both were removed from the DIP for the next review round.

This version proposed the syntax in assert(arg) and out(ret) assert(ret). This syntax received negative feedback for being too significant a change and too dissimilar to the syntax of other D language features. This proposed syntax was replaced in the next iteration of the DIP.

Preliminary Review Round 2

Reviewed Version

Discussion

The overall feedback for the proposed syntax in this revision of the DIP was positive. It was noted that an example of the syntax in a bodyless function should be provided, so one was added in the next iteration of the DIP.

Final Review

Reviewed Version

Discussion

No revisions were made to the DIP as a result of this review round and the DIP was submitted without changes for Formal Assessment.

Formal Assessment

Reviewed Version A

Reviewed Version B

Reviewed Version C

The Language Maintainers approved of the proposed feature without objection, but found the language of the DIP as it existed in Version A to be below the standards expected of a quality proposal. A further round of revisions by both the DIP Author and Jared Hanson resulted in Version B. This version still failed to meet the expected standards. After further revision by Timon Gehr, the DIP was accepted with minor edits by the Language Maintainers.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

DIP1009.md

DIP1009.md

Add Expression-Based Contract Syntax

Abstract

Links

Rationale

Description

New `out` syntax

Grammar

Code Breakage

Acknowledgments

Copyright & License

Reviews

Preliminary Review Round 1

Preliminary Review Round 2

Final Review

Formal Assessment

Files

DIP1009.md

Latest commit

History

DIP1009.md

File metadata and controls

Add Expression-Based Contract Syntax

Abstract

Links

Rationale

Description

New out syntax

Grammar

Code Breakage

Acknowledgments

Copyright & License

Reviews

Preliminary Review Round 1

Preliminary Review Round 2

Final Review

Formal Assessment

New `out` syntax