Documentation
¶
Overview ¶
Package contract provides contract related objects
Index ¶
- Variables
- func ExpandEnsuresExpression(expression Expression) (shortStmt, expr string, idToOldIDMap map[string]string)
- type Ensures
- type Expression
- type FuncContract
- func (c *FuncContract) AddEnsures(e Ensures) *FuncContract
- func (c *FuncContract) AddImport(path string) *FuncContract
- func (c *FuncContract) AddLet(l Let) *FuncContract
- func (c *FuncContract) AddRequires(r Requires) *FuncContract
- func (c *FuncContract) Ensures() (r []Ensures)
- func (c *FuncContract) Imports() map[string]struct{}
- func (c *FuncContract) IsEmpty() bool
- func (c *FuncContract) Lets() (r []Let)
- func (c *FuncContract) Requires() (r []Requires)
- type Let
- type Requires
- type TypeContract
- func (c *TypeContract) AddEnsures(e Ensures) *TypeContract
- func (c *TypeContract) AddImport(path string) *TypeContract
- func (c *TypeContract) AddRequires(r Requires) *TypeContract
- func (c *TypeContract) Ensures() (r []Ensures)
- func (c *TypeContract) Imports() (r map[string]struct{})
- func (c *TypeContract) IsEmpty() bool
- func (c *TypeContract) Requires() (r []Requires)
Constants ¶
This section is empty.
Variables ¶
var OldCounter = 0
OldCounter the counter to use when creating old_ parameters TODO: use a more elegant approach
var Re4old = regexp.MustCompile(`@old\{(.+)\}`)
Re4old is a regular expression for @old expressions.
Functions ¶
func ExpandEnsuresExpression ¶ added in v0.3.0
func ExpandEnsuresExpression(expression Expression) (shortStmt, expr string, idToOldIDMap map[string]string)
Types ¶
type Ensures ¶
type Ensures struct {
// contains filtered or unexported fields
}
Ensures is a @ensures clause of a contract.
Contract:
- invariant Ensures.expr != ""
func NewEnsures ¶
func NewEnsures(expr Expression, description string) (r Ensures)
NewEnsures creates a Ensures object.
Contract:
- requires expr != ""
- ensures r.expr == expr
- ensures r.description == description
func (Ensures) Description ¶
Description yields the description of this Ensures.
func (Ensures) ExpandedExpression ¶
ExpandedExpression yields the expanded ensures' expression.
Contract:
- ensures expr != ""
- ensures idToOldIdMap != nil
func (Ensures) Expression ¶
func (r Ensures) Expression() (expr Expression)
Expression yields the expression of this Ensures.
type Expression ¶ added in v0.3.0
type Expression struct {
Raw string
}
type FuncContract ¶
type FuncContract struct {
// contains filtered or unexported fields
}
FuncContract represents a contract associated to a function.
Contract:
- invariant FuncContract.requires != nil
- invariant FuncContract.ensures != nil
- invariant FuncContract.import != nil
- invariant FuncContract.lets != nil
- invariant FuncContract.target != nil
func NewFuncContract ¶
func NewFuncContract() (c *FuncContract)
NewFuncContract creates a FuncContract.
Contract:
- ensures len(c.requires) == 0
- ensures len(c.ensures) == 0
- ensures len(c.imports) == 0
- ensures len(c.lets) == 0
func (*FuncContract) AddEnsures ¶
func (c *FuncContract) AddEnsures(e Ensures) *FuncContract
AddEnsures adds a ensures to this contract.
Contract:
- ensures len(c.ensures) == @old{len(c.ensures)} + 1
- ensures c.ensures[len(c.ensures)-1] == e
func (*FuncContract) AddImport ¶
func (c *FuncContract) AddImport(path string) *FuncContract
AddImport adds an import to this contract.
Contract:
- requires path != ""
- ensures len(c.imports) >= @old{len(c.imports)}
func (*FuncContract) AddLet ¶
func (c *FuncContract) AddLet(l Let) *FuncContract
AddLet adds a Let to this contract.
Contract:
- ensures len(c.lets) == @old{len(c.lets)} + 1
- ensures c.lets[len(c.lets)-1] == l
func (*FuncContract) AddRequires ¶
func (c *FuncContract) AddRequires(r Requires) *FuncContract
AddRequires adds a requires to this contract. Contract:
- ensures len(c.requires) == @old{len(c.requires)} + 1
- ensures c.requires[len(c.requires)-1] == r
func (*FuncContract) Ensures ¶
func (c *FuncContract) Ensures() (r []Ensures)
Ensures yields ensures clauses of this contract.
Contract:
- ensures len(r) == len(c.ensures)
- unmodified len(c.ensures)
func (*FuncContract) Imports ¶
func (c *FuncContract) Imports() map[string]struct{}
Imports returns imports required by this contract.
Contract:
- ensures len(r) == len(c.imports)
func (*FuncContract) IsEmpty ¶
func (c *FuncContract) IsEmpty() bool
IsEmpty returns true if this contract doesn't have requires nor ensure clauses, false otherwise.
func (*FuncContract) Lets ¶
func (c *FuncContract) Lets() (r []Let)
Lets yields lets clauses of this contract. Contract:
- ensures len(r) == len(c.lets)
func (*FuncContract) Requires ¶
func (c *FuncContract) Requires() (r []Requires)
Requires yields requires clauses of this contract. Contract:
- ensures len(r) == len(c.requires)
- unmodified len(c.requires)
type Let ¶
type Let struct {
// contains filtered or unexported fields
}
Let models a @Let clause.
func NewLet ¶
func NewLet(expr Expression, description string) Let
NewLet creates a Let object
Contract:
- requires expr != ""
func (Let) ExpandedExpression ¶
func (l Let) ExpandedExpression() Expression
ExpandedExpression yields the expanded let expression
type Requires ¶
type Requires struct {
// contains filtered or unexported fields
}
Requires is a @requires clause of a contract
func NewRequires ¶
func NewRequires(expr Expression, description string) Requires
NewRequires creates a Requires object.
Contract:
- requires expr != ""
func (Requires) Description ¶
Description yields the description of this Requires.
func (Requires) ExpandedExpression ¶
func (r Requires) ExpandedExpression() (result Expression)
ExpandedExpression yields the expanded requires' expression.
Contract:
- ensures result != ""
func (Requires) Expression ¶
func (r Requires) Expression() (expr Expression)
Expression yields the expression of this Requires.
type TypeContract ¶
type TypeContract struct {
// contains filtered or unexported fields
}
TypeContract represents a contract associated to a type. Typically a @invariant contract.
Contract:
- invariant TypeContract.ensures != nil
- invariant TypeContract.requires != nil
- invariant TypeContract.imports != nil
- invariant TypeContract.targetTypeName != nil
func NewTypeContract ¶
func NewTypeContract(target string) (c *TypeContract)
NewTypeContract creates a TypeContract.
Contract:
- requires target != ""
- ensures c.targetTypeName == target
- ensures c.ensures != nil && len(c.ensures) == 0
- ensures c.requires != nil && len(c.requires) == 0
- ensures c.imports != nil && len(c.imports) == 0
func (*TypeContract) AddEnsures ¶
func (c *TypeContract) AddEnsures(e Ensures) *TypeContract
AddEnsures adds a ensures to this contract.
Contract:
- requires e != nil
- ensures len(c.ensures) == @old{len(c.ensures})} + 1
- ensures c.ensures[len(c.ensures)-1] == e
func (*TypeContract) AddImport ¶
func (c *TypeContract) AddImport(path string) *TypeContract
AddImport adds an import to this contract.
Contract:
- requires path != ""
- ensures len(c.imports) >= @old{len(c.imports)}
func (*TypeContract) AddRequires ¶
func (c *TypeContract) AddRequires(r Requires) *TypeContract
AddRequires adds a requires to this contract.
Contract:
- ensures len(c.requires) == @old{len(c.requires)} + 1
- ensures c.requires[len(c.requires)-1] == r
func (*TypeContract) Ensures ¶
func (c *TypeContract) Ensures() (r []Ensures)
Ensures yields ensures clauses of this contract.
Contract:
- ensures len(r) == len(c.ensures)
func (*TypeContract) Imports ¶
func (c *TypeContract) Imports() (r map[string]struct{})
Imports returns imports required by this contract.
Contract:
- ensures len(r) == len(c.imports)
func (*TypeContract) IsEmpty ¶
func (c *TypeContract) IsEmpty() bool
IsEmpty returns true if this contract doesn't have requires nor ensure clauses, false otherwise.
func (*TypeContract) Requires ¶
func (c *TypeContract) Requires() (r []Requires)
Requires yields requires clauses of this contract.
Contract:
- ensures len(r) == len(c.requires)
Source Files
Directories