Contracts

[gbracha]

See Eiffel for an example of core language support, C#/.NET and Java (including http://go/cofoja developed at Google) for less pretty but fully functional implementations.

This is a complex feature, filing now so it can be considered at the appropriate time.

(It might appeal to the people who have been asking for non nullable types.)

The major pieces that are needed are:

1. Tagging with predicates
   1.1 Tagging of classes with predicates: invariants
   1.2 Tagging of methods with predicates: preconditions, postconditions, (exceptional postconditions)
2. New keywords or functions for use in postconditions
   2.1 "result" refers to the method result
   2.2 "old(foo)" refers to the value of foo on method entry
3. Contract evaluation at runtime: execute before and after method invocations
   3.1 But not when evaluating a contract predicate
   3.2 With facility to enable/disable contracts by library
   3.3 With invariants ignored for "private" method calls (whatever this means for Dart)
   3.4 Inheriting contract predicates from superclasses, interfaces
4. A way to disable contracts and have the code execute as quickly as if there were no contracts

[gbracha]

The feature was requested by David Morgan; I am generally sympathetic in principle, but do nor expect this to happen for some time (if ever). It is a complex topic.

---

Added this to the Later milestone.

[gbracha]

Added Area-Language label.

[DartBot]

This comment was originally written by [email protected]

---

Thanks for filing on my behalf.

The full link for cofoja is http://code.google.com/p/cofoja/

[DartBot]

This comment was originally written by [email protected]

---

This was for many years in the top 25 RFE for Java (http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=4449383).

Contracts can quickly become very complex and perhaps there's a law of diminishing returns, but they have a good deal of value.

All code has a contract. Most code has an implicit contract: this means a reader must READ THE CODE (all of it) to understand what it does. This makes for much lower productivity in the long-run.

DbC just makes the contract explicit rather than relying upon
a) JavaDoc (etc) comments which are prone to becoming out-of-date or
b) unit-tests which are separate too and often densely written (lack of clarity).
c) reading the code top-to-bottom

My experience of DbC has interesting parallels with unit-testing in that they both result in the developer writing smaller, tighter classes.

Another useful benefit of DbC is that static analysis tools can make a much more reasonable analysis.

If DbC doesn't happen (as I expect it won't), then Dart should at least add non-null types (http://code.google.com/p/dart/issues/detail?id=22).

Source code expressing correctness is a good thing.

This link outlines DbC: http://www.eiffel.com/developers/design_by_contract.html

[DartBot]

This comment was originally written by [email protected]

---

Maybe some simple way to mark type annotations and asserts as part of library api contract - which are used in production mode:

@contract int test(int x) {
   @­contract assert (x > 1 && x < 100);

}

[DartBot]

This comment was originally written by [email protected]

---

Library based solution? https://groups.google.com/a/dartlang.org/forum/?fromgroups#!topic/misc/w02qkmFYqE0

[kasperl]

Removed this from the Later milestone.
Added Oldschool-Milestone-Later label.

[kasperl]

Removed Oldschool-Milestone-Later label.

[gbracha]

Issue #15390 has been merged into this issue.

[chalin]

FYI. The addition of native C# support for method contracts was discussed at the Jan 21, 2015 C# Design Meeting. The issue used to track this specific feature is dotnet/roslyn#119.