Documentation
¶
Overview ¶
Package contract provides contract related objects
Index ¶
- type Ensures
- type FuncContract
- func (c *FuncContract) AddEnsures(e Ensures)
- func (c *FuncContract) AddImport(path string)
- func (c *FuncContract) AddRequires(r Requires)
- func (c *FuncContract) Ensures() (r []Ensures)
- func (c *FuncContract) Imports() map[string]struct{}
- func (c *FuncContract) Requires() (r []Requires)
- func (c *FuncContract) Target() (t *ast.FuncDecl)
- type Requires
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type Ensures ¶
type Ensures struct {
// contains filtered or unexported fields
}
Ensures is a @ensures clause of a contract
func NewEnsures ¶
NewEnsures creates a Ensures object @ensures expr != ""
func (Ensures) ExpandedExpression ¶
ExpandedExpression yields the expanded ensures' expression
type FuncContract ¶
type FuncContract struct {
// contains filtered or unexported fields
}
FuncContract represents a contract associated to a function
func NewFuncContract ¶
func NewFuncContract(target *ast.FuncDecl) (c FuncContract)
NewFuncContract creates a FuncContract @requires target != nil @ensures c.target == target @ensures len(c.requires) == 0 @ensures len(c.ensures) == 0 @ensures len(c.imports) == 0
func (*FuncContract) AddEnsures ¶
func (c *FuncContract) AddEnsures(e Ensures)
AddEnsures adds a ensures to this contract @ensures len(c.ensures) == len(@old(c.ensures)) + 1 @ensures c.ensures[len(c.ensures)-1] == e
func (*FuncContract) AddImport ¶
func (c *FuncContract) AddImport(path string)
AddImport adds an import to this contract
func (*FuncContract) AddRequires ¶
func (c *FuncContract) AddRequires(r Requires)
AddRequires adds a requires to this contract @ensures len(c.requires) == len(@old(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 @ensures len(r) == len(c.ensures)
func (*FuncContract) Imports ¶
func (c *FuncContract) Imports() map[string]struct{}
Imports returns imports required by this contract
func (*FuncContract) Requires ¶
func (c *FuncContract) Requires() (r []Requires)
Requires yields requires clauses of this contract @ensures len(r) == len(c.requires)
func (*FuncContract) Target ¶
func (c *FuncContract) Target() (t *ast.FuncDecl)
Target yields the function declaration to which this contract is attached to @ensures t == c.target
type Requires ¶
type Requires struct {
// contains filtered or unexported fields
}
Requires is a @requires clause of a contract
func NewRequires ¶
NewRequires creates a Requires object @requires expr != ""
func (Requires) ExpandedExpression ¶
ExpandedExpression yields the expanded requires' expression
Source Files
Directories