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.
Logo by Eze
Contracts are embedded into comments, therefore code annotated with contracts is still valid GO code.
This project uses contracts itself! Check the source code and the Makefile to see how.
You can also check the examples.
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 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 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 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 ==> operator (implication) allows 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) { ... }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 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 identifiers list
contract:import pakage name