Documentation
¶
Overview ¶
Package examples provides examples of using contracts
Index ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type BankAccount ¶
type BankAccount struct {
// contains filtered or unexported fields
}
BankAccount represents a bank account.
Contract:
- invariant balance of open accounts is always at least the minBalance: !BankAccount.closed ==> BankAccount.balance >= minBalance
- invariant balance of open accounts is always at most the maxBalance: !BankAccount.closed ==> BankAccount.balance <= maxBalance
- invariant balance of closed accounts is 0: BankAccount.closed ==> BankAccount.balance == 0
func NewBankAccount ¶
func NewBankAccount(initialBalance int) (account BankAccount)
NewBankAccount creates an account with the given initial balance.
Contract:
- requires initialBalance >= minBalance && initialBalance <= maxBalance
- ensures account.balance == initialBalance
- ensures !account.closed
func (*BankAccount) Balance ¶
func (a *BankAccount) Balance() (balance int)
Balance yields the balance of the account.
Contract:
- ensures balance == a.balance
- unmodified a.balance
- unmodified a.closed
func (*BankAccount) Close ¶
func (a *BankAccount) Close() (payout int)
Close the account and returns its payout.
Contract:
- requires !a.closed
- ensures payout == @old{a.balance}
- ensures a.closed
- ensures a.balance == 0
func (*BankAccount) Credit ¶
func (a *BankAccount) Credit(amount int)
Credit the given amount to the account.
Contract:
- requires can not credit a closed account: !a.closed
- requires amount > 0 && (a.balance + amount) <= maxBalance
- let initialBalance := a.balance
- ensures a.balance == initialBalance + amount
- unmodified a.closed
func (*BankAccount) Debit ¶
func (a *BankAccount) Debit(amount int)
Debit the given amount from the account.
Contract:
- requires !a.closed
- requires amount > 0 && (a.balance - amount) >= minBalance
- let initialBalance := a.balance
- ensures a.balance == initialBalance - amount
- unmodified a.closed
type Set ¶
type Set struct {
// contains filtered or unexported fields
}
Set is a collection of unique elements.
Contract:
- invariant Set.elements != nil
func NewSet ¶
func NewSet() (s *Set)
NewSet creates a new set.
Contract:
- ensures s.elements != nil && len(s.elements) == 0
func (*Set) Add ¶
Add inserts an element into the set.
Contract:
- ensures element is present in the set: s.Contains(value)
- let alreadyPresent := s.Contains(value)
- ensures cardinality grows if new element: !alreadyPresent ==> @old{len(s.elements)} == len(s.elements) - 1
- ensures cardinality remains the same if no new element: alreadyPresent ==> @old{len(s.elements)} == len(s.elements)
func (*Set) Contains ¶
Contains checks if an element is in the set.
Contract:
- ensures _, ok := s.elements[value]; ok ==> result == true
- ensures _, ok := s.elements[value]; !ok ==> result != true
- unmodified len(s.elements)
func (*Set) List ¶
List returns all elements in the set as a slice.
Contract:
- ensures len(result) == len(s.elements)
- unmodified len(s.elements)
func (*Set) Remove ¶
Remove deletes an element from the set.
Contract:
- ensures element is not present in the set: !s.Contains(value)
- let alreadyPresent := s.Contains(value)
- ensures cardinality shirks if element was in the set: alreadyPresent ==> @old{len(s.elements)-1} == len(s.elements)
- ensures cardinality remains the same if element was not in the set: !alreadyPresent ==> @old{len(s.elements)} == len(s.elements)
type Stack ¶
type Stack struct {
// contains filtered or unexported fields
}
Stack implementation borrowed from https://dev.to/jpoly1219/stacks-in-go-54k
func (*Stack) IsEmpty ¶
IsEmpty returns true if the stack has no data, false otherwise.
Contract:
- let size := len(s.items)
- ensures if empty then true: size == 0 ==> result == true
- ensures if not empty then false: size != 0 ==> result == false
- unmodified stack size: len(s.items)
func (*Stack) Pop ¶
func (s *Stack) Pop()
Pop pops the top element from the stack.
Contract:
- requires non empty stack: !s.IsEmpty()
- ensures stack shrinks by one element: @old{len(s.items)} == len(s.items) + 1
func (*Stack) Push ¶
Push pushes data in the stack.
Contract:
- ensures stack grows by one element: @old{len(s.items)} == len(s.items) - 1
- ensures new data is on top of the stack: s.Top() == data
Source Files
Directories