Design by Contract™ for GO is a code generator that takes GO code annotated with contracts and generates code that enforces those contracts at runtime.
Contracts are embedded into comments, therefore code annotated with contracts is still valid GO code.
Logo by Eze
A simple example: imagine you have a counter type like the following
type Counter struct {
value int
}
// IncrementBy increments the counter value by n.
func (c *Counter) IncrementBy(n int) {
c.value += n
}You can add a contract to the IncrementBy method to enforce that the resulting value of the counter is actually incremented by n at the end of method's execution:
// IncrementBy increments the counter value by n.
//
// Contract:
// - ensures value is incremented by n: c.value == @old{c.value} + n
func (c *Counter) IncrementBy(n int) {
c.value += n
}As is, the contract you added has no effect on your code other than better documenting it.
But if you run dbc4go on the source file (let's say counter.go)
$ dbc4go -i counter.go
you will get the following code:
type Counter struct {
value int
}
// Increment increments the counter value by a n.
//
// Contract:
// - ensures value is incremented by n: c.value == @old{c.value} + n
func (c *Counter) IncrementBy(n int) {
{ // Open contract scope
// Function's contracts
old_1 := c.value
defer func() {
if !(c.value == old_1+n) {
panic("function didn't ensure value is incremented by n")
}
}()
} // Close contract scope
c.value += n
}As you can see, dbc4go instrumented the original code by adding a whole block of statements at the beginning of the method's body.
The new code block implements the checking of the contract you wrote in the documentation of the method.
Now, when the instrumented version of your code is executed, the contract will be enforced, and if the contract is not respected the method will panic.
For further information on how to write contracts you can read the section Available contract clauses below and check the examples.
You might still wonder how this can be useful for you.
Well, one thing you can do is execute your tests on the instrumented version of your code.
You could, for example, use go generate to obtain an instrumented version of your files and then run go test.
Like that, tests and contracts will combine to provide you more chances to find bugs.
This project uses contracts itself! Check the source code and the Makefile to see how.
The article Design by Contract by Bertrand Meyer provides a complete and clear explanation of the idea.
Just grab the executable corresponding to your platform from the releases page (here on the right ----> )
Usage of dbc4go:
-i string
input source file (defaults to stdin)
-o string
output file (defaults to stdout)
requires contract clauses describe pre-conditions imposed by functions/methods.
Syntax:
requires(description:)? GO Boolean expression
As you can see in the example below, the GO Boolean expression must be a valid GO Boolean expression as it will be used as the condition in an if-then statement.
The expression can make reference to any identifier available in the scope at the beginning of the annotated function (for example: function parameters, method receiver, global variables, other functions)
Contract clauses must be organized as a list under a contract declaration of the form Contract:.
Example:
const maxAuthorizedSpeed = 350
// NewCar returns a Car struct.
//
// Contract:
// - requires more than 2 wheels: wheels > 2
// - requires wheelsDrive <= wheels && wheelsDrive >= 2 && wheelsDrive%2 == 0
// - requires maxSpeedKmh > 0 && maxSpeedKmh <= maxAuthorizedSpeed
// - requires manufacturer != ""
func NewCar(wheels int, wheelsDrive int, maxSpeedKmh int, manufacturer string) Car { ... }Short-statements are supported as part of GO Boolean expression, therefore it's okay to write a contract like the following:
// Accelerate the car.
//
// Contract:
// - requires delta > 0
// - requires targetSpeed := c.speed + delta; targetSpeed <= c.maxSpeedKmh
func (c *Car) Accelerate(delta int) { ... }ensures contract clauses describes post-conditions of a function/method.
Syntax:
ensures (description:)? GO Boolean expression
As for ensure clauses, the expression can make reference to any identifier available in the scope at the beginning of the annotated function (for example: function parameters, method receiver, global variables, other functions).
Additionally, expressions in ensure clauses can use the @old operator to refer to the state of variables as it was just before the execution of the function.
Example:
// Accelerate the car.
//
// Contract:
// - requires delta > 0
// - requires c.speed + delta <= c.maxSpeedKmh
// - ensures c.speed == @old{c.speed}+delta
func (c *Car) Accelerate(delta int) { ... }Limitations of @old:
- at most one
@oldexpression in the short-statement and one in the Boolean expression. dbc4godoesn't have type information of expressions inside an@oldannotation therefore in some cases you need to add type casts to obtain compilable code. For example, to indicate that@old{someExpression}is of typefloatyou must write@old{someExpression}.(float)
An alternative to @old annotations is the use of let clauses (see below) thus the previous example could be also written as:
// Accelerate the car.
//
// Contract:
// - requires delta > 0
// - requires c.speed + delta <= c.maxSpeedKmh
// - let initialSpeed := c.speed
// - ensures c.speed == initialSpeed+delta
func (c *Car) Accelerate(delta int) { ... }Captures an expression's value into a variable at the beginning of the function execution.
The variable can be used in ensures and requires
Syntax:
let id := expression
id must be a valid GO identifier and expression a valid GO expression in the context of the annotated function.
Defines an invariant property of a struct.
An invariant property is a property of the struct that should always hold.
Every method attached to the struct can assume the invariants hold and must preserve the invariants.
Invariants are enforced, materialized as requires and ensures clauses, on every method attached to the struct.
Syntax:
invariant (description:)? GO Boolean expression
The expression can make reference to any identifier available in the scope of the struct declaration and any private field identifier of the struct to which the invariant applies to.
References to fields must be a selector expression of the form <struct-name>.<field-name>
Examples:
// Car data-model.
//
// Contract:
// - invariant Car.speed <= Car.maxSpeedKmh
// - invariant Car.speed >= 0
type Car struct {
maxSpeedKmh int
speed int
// other fields ...
}// BankAccount data-model
//
// Contract:
// - invariant BankAccount.balance >= 0
type BankAccount struct {
balance float
// other fields ...
}Enforces the function keeps unmodified the given list of expressions.
Syntax:
unmodified (description:)? expressions list
Example:
// Accelerate the car.
//
// Contract:
// - requires delta > 0
// - requires c.speed + delta <= c.maxSpeedKmh
// - let initialSpeed := c.speed
// - ensures c.speed == initialSpeed+delta
// - unmodified c.wheels, c.wheelsDrive, c.maxSpeedKmh, c.manufacturer
func (c *Car) Accelerate(delta int) { ... }unmodified is just syntax sugar for simplify writing ensures expr == @old{expr}
If in your contracts you need to use a package that is not imported by the original source code, then you can import the package with the import clause.
Syntax:
import pakage name
Example:
// Add element e to container
//
// Contract:
// - import strings
// - requires strings.HasPrefix(e, "my")
func (c *Container) Add(e string) { ... }The ==> (implication) and <==> (double implication) allow to write more precise and concise contracts like
// Accelerate the car.
//
// Contract:
// - requires delta > 0
// - let initialSpeed := c.speed
// - ensures initialSpeed + delta < c.maxSpeedKmh ==> c.speed == initialSpeed + delta
// - ensures initialSpeed + delta >= c.maxSpeedKmh ==> c.speed == c.maxSpeedKmh
func (c *Car) Accelerate(delta int) { ... }The @forall operator allows to write contracts on all the elements of a collection (a range-able type)
Syntax:
@forall element_id (@in|@indexof|@iterating) collection_id: GO Boolean expression
While the syntax @forall ... @in shall be used when ranging over elements of the collection; @forall ... @indexof shall be used when iterating with an index over the collection and @iterating must be used when ranging through an iterator functions.
// square returs the square of the given integers
//
// Contract:
// - ensures all returned elements are non-negative: @forall n @in squareds: n >= 0
func square(nums []int) (squareds []int) {
// implementation
}// square returs the square of the given integers
//
// Contract:
// - ensures @forall i @indexof nums: squareds[i] == nums[i] * nums[i]
func square(nums []int) (squareds []int) {
// implementation
}The @exists operator allows to write contracts on the elements of a collection (a range-able type)
Syntax:
@exists element_id (@in|@indexof|@iterating) collection_id: GO Boolean expression
Choosing between @in, @indexof and @iterating follows the same rules as within the @forall operator.
@forall and @exists operators can be nested with the following syntax:
((@forall|@exists) element_id (@in|@indexof) collection_id:)+ GO Boolean expression
dbc4go supports three contract syntaxes:
- standard syntax, the one introduced in the previous sections,
- raw syntax, and
- directive syntax
All three syntaxes have equivalent expressiveness power.
While the raw syntax is easier/shorter to write, the standard syntax lets GO tools and IDE to render function and types contracts in a nicer and readable form.
// Contract in standard syntax
// NewCar returns a Car struct.
//
// Contract:
// - requires wheels > 2
// - requires wheelsDrive <= wheels && wheelsDrive >= 2 && wheelsDrive%2 == 0
// - requires maxSpeedKmh > 0 && maxSpeedKmh <= maxAuthorizedSpeed
// - requires manufacturer != ""
func NewCar(...) {...}// Contract in raw syntax
// NewCar returns a Car struct.
//
// @requires wheels > 2
// @requires wheelsDrive <= wheels && wheelsDrive >= 2 && wheelsDrive%2 == 0
// @requires maxSpeedKmh > 0 && maxSpeedKmh <= maxAuthorizedSpeed
// @requires manufacturer != ""
func NewCar(...) {...}Raw syntax doesn't require a contract declaration, and contract clauses can be line-interleaved within non-contractual documentation.
Directive syntax is useful in situations where you need to add a contract clause that will not render in the documentation. For example, if a struct invariant refers to a private field and you don't want to leak the field's name in the documentation you can define the invariant using directive syntax:
// Contract in directive syntax
// BankAccount represents a bank account.
//
//contract:invariant !BankAccount.closed ==> BankAccount.balance >= minBalance
//contract:invariant !BankAccount.closed ==> BankAccount.balance <= maxBalance
//contract:invariant BankAccount.closed ==> BankAccount.balance == 0
type BankAccount struct {
balance int // the balance of the account
closed bool // is the account closed?
}(notice there is no blank space between the comment delimiter // and the contract clause)
@requires (description:)? GO Boolean expression
@ensures (description:)? GO Boolean expression
@let id := expression
@invariant (description:)? GO Boolean expression
@unmodified (description:)? identifiers list
@import pakage name
You can check these examples of code annotated with the raw syntax.
Contract clauses must respect the directive comment format as defined in the Syntax section of Go Doc Comments
contract:requires (description:)? GO Boolean expression
contract:ensures (description:)? GO Boolean expression
contract:let id := expression
contract:invariant (description:)? GO Boolean expression
contract:unmodified (description:)? identifiers list
contract:import pakage name
