contract

package
v1.5.12 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Mar 3, 2026 License: MIT Imports: 5 Imported by: 0

Documentation

Overview

Package contract provides function behavior specifications using Hoare-style contracts.

A contract (Spec) specifies the complete behavioral interface of a function:

Preconditions (Requires): Constraints that must hold at the call site. The type checker verifies these at each call and reports errors when preconditions cannot be proven. 

-- Precondition: first argument must be non-nil
function assert_not_nil(x)
    if x == nil then error("nil!") end
    return x
end

Postconditions (Ensures): Facts that become true after the call returns. The type checker adds these to the type environment for subsequent code, enabling narrowing. 

-- Postcondition: return value is non-nil
local y = assert_not_nil(x)  -- y is narrowed to non-nil

Effects: Type-level side effects from types/effect, including mutations, return type derivations, and control effects like throw/diverge.

Callbacks: Specifications for callback parameters, describing how they are invoked (cardinality), what they return (boolean for predicates), and whether they are pure.

Return specifications: Conditional return types based on argument conditions, enabling precise return types that depend on runtime values.

Usage: 

spec := contract.NewSpec().
    WithRequires(constraint.NotNil{Path: constraint.Path{Root: "p0"}}).
    WithEnsures(constraint.NotNil{Path: constraint.Path{Root: "r0"}}).
    WithEffects(effect.Throw{})

fn := typ.Func().Param("x", typ.Any).Returns(typ.Any).Spec(spec).Build()

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

This section is empty.

Types

type CallbackSpec 

type CallbackSpec struct {
	// InputSource references the parameter providing input to the callback.
	InputSource effect.ParamRef
	// ReturnsBoolean indicates the callback returns a boolean (predicate).
	ReturnsBoolean bool
	// Cardinality describes how many times the callback is invoked.
	Cardinality Cardinality
	// Pure indicates the callback has no side effects.
	Pure bool
	// EnvOverlay describes callback-scoped globals injected into the callback environment.
	EnvOverlay map[string]typ.Type
}

CallbackSpec describes a callback parameter's expected behavior.

CallbackSpec enables precise typing of higher-order functions by describing how a callback is used:

For table.filter(t, predicate): 

CallbackSpec{
    InputSource:    ParamRef{Index: 0},  // callback receives elements from t
    ReturnsBoolean: true,                // callback is a predicate
    Cardinality:    CardAtMostOncePerElement,
    Pure:           true,
}

This enables the type checker to:

  • Infer callback parameter types from InputSource
  • Verify callback return type matches ReturnsBoolean
  • Track cardinality for escape analysis
  • Inject EnvOverlay bindings into callback scope

func MapperSpec 

func MapperSpec(inputParam int) *CallbackSpec

MapperSpec creates a callback spec for mapping functions.

func PredicateSpec 

func PredicateSpec(inputParam int) *CallbackSpec

PredicateSpec creates a callback spec for predicate functions.

func (*CallbackSpec) Clone 

func (c *CallbackSpec) Clone() *CallbackSpec

Clone returns a deep copy of the CallbackSpec.

func (*CallbackSpec) Equals 

func (c *CallbackSpec) Equals(other *CallbackSpec) bool

Equals returns true if two CallbackSpec values are structurally equal.

func (*CallbackSpec) WithEnvOverlay 

func (c *CallbackSpec) WithEnvOverlay(env map[string]typ.Type) *CallbackSpec

WithEnvOverlay sets callback-scoped globals.

type Cardinality 

type Cardinality int

Cardinality describes invocation count for callbacks.

Cardinality is used for escape analysis and optimization. A callback that is only called once per element may have different optimization opportunities than one called an unknown number of times. 

const (
	// CardOncePerElement: callback is called exactly once per input element.
	// Used by table.map, table.foreach.
	CardOncePerElement Cardinality = iota
	// CardAtMostOncePerElement: callback may be called 0 or 1 times per element.
	// Used by table.filter (stops on first match in some variants).
	CardAtMostOncePerElement
	// CardExactlyOnce: callback is called exactly once total.
	// Used by pcall, xpcall.
	CardExactlyOnce
	// CardAtMostOnce: callback may be called 0 or 1 times total.
	// Used by table.find (calls predicate until match).
	CardAtMostOnce
	// CardUnknown: invocation count is not known.
	// Conservative default for user-defined higher-order functions.
	CardUnknown
)

func (Cardinality) String 

func (c Cardinality) String() string

type ReturnCase 

type ReturnCase struct {
	// When is the condition under which this return type applies.
	When constraint.Condition
	// Type is the refined return type when the condition holds.
	Type typ.Type
}

ReturnCase describes a conditional return type.

A ReturnCase pairs a condition with a return type. When the condition can be proven from the call context, the associated type is used instead of the default return type.

func (ReturnCase) Equals 

func (r ReturnCase) Equals(other ReturnCase) bool

Equals returns true if two ReturnCase values are structurally equal.

type ReturnSpec 

type ReturnSpec struct {
	// Cases holds condition-dependent return type refinements.
	Cases []ReturnCase
	// Default is the return type when no case condition matches.
	Default typ.Type
}

ReturnSpec describes conditional return types.

ReturnSpec enables overload-like behavior where the return type depends on the argument types or values. Cases are checked in order; the first matching condition determines the return type.

Example for tonumber(s): 

ReturnSpec{
    Cases: []ReturnCase{
        {When: HasType{p0, integer}, Type: integer},  // integer input
        {When: HasType{p0, number}, Type: number},    // number input
    },
    Default: typ.NewOptional(typ.Number),  // string input may fail
}

func (*ReturnSpec) Equals 

func (r *ReturnSpec) Equals(other *ReturnSpec) bool

Equals returns true if two ReturnSpec values are structurally equal.

type Spec 

type Spec struct {
	// Requires holds preconditions that must be satisfied at call site.
	// Checked by the type checker before the call; errors if not provable.
	Requires constraint.Condition
	// Ensures holds postconditions that become facts after the call returns.
	// Added to the type environment for code following the call.
	Ensures constraint.Condition
	// ExprRequires holds arithmetic preconditions on parameters.
	// Used for length/index bounds checking.
	ExprRequires []constraint.ExprCompare
	// ExprEnsures holds arithmetic postconditions on return values.
	// Used for return length guarantees.
	ExprEnsures []constraint.ExprCompare
	// Effects describes type-level side effects (mutations, returns).
	// See types/effect for the effect label vocabulary.
	Effects effect.Row
	// Callbacks maps parameter indices to their callback specifications.
	// Key is the 0-based parameter index of the callback.
	Callbacks map[int]*CallbackSpec
	// Return describes conditional return type refinements.
	// Enables different return types based on argument conditions.
	Return *ReturnSpec
}

Spec is the complete specification of a function's behavior.

A Spec captures everything the type checker needs to know about a function's contract with its callers. This information enables:

  • Precondition checking at call sites
  • Type narrowing from postconditions
  • Effect propagation through call chains
  • Precise return type derivation
  • Higher-order function analysis via callback specs

func ExtractSpec 

func ExtractSpec(t typ.Type) *Spec

ExtractSpec unwraps a function type and returns its contract spec, or nil.

func NewSpec 

func NewSpec() *Spec

NewSpec creates an empty spec.

func (*Spec) EffectRow 

func (s *Spec) EffectRow() effect.Row

EffectRow returns the effect row.

func (*Spec) Equals 

func (s *Spec) Equals(other any) bool

Equals returns true if two Specs are structurally equal. Implements internal.Equaler interface for use in typ.Function.

func (*Spec) GetCallback 

func (s *Spec) GetCallback(paramIdx int) *CallbackSpec

GetCallback returns the callback spec for a parameter.

func (*Spec) GetIterator 

func (s *Spec) GetIterator() *effect.Iterator

GetIterator returns the iterator effect.

func (*Spec) GetMutation 

func (s *Spec) GetMutation() *effect.Mutate

GetMutation returns the first mutation effect.

func (*Spec) GetMutationAt 

func (s *Spec) GetMutationAt(paramIdx int) *effect.Mutate

GetMutationAt returns the mutation effect for a specific parameter.

func (*Spec) GetReturnCases 

func (s *Spec) GetReturnCases() []ReturnCase

GetReturnCases returns conditional return cases.

func (*Spec) GetReturnDefault 

func (s *Spec) GetReturnDefault() typ.Type

GetReturnDefault returns the default return type if set.

func (*Spec) GetReturnLength 

func (s *Spec) GetReturnLength(retIdx int) *effect.ReturnLength

GetReturnLength returns the return length effect.

func (*Spec) GetReturnType 

func (s *Spec) GetReturnType(retIdx int) *effect.Return

GetReturnType returns the return type effect.

func (*Spec) GetTableMutator 

func (s *Spec) GetTableMutator() *effect.TableMutator

GetTableMutator returns the table mutator effect.

func (*Spec) HasMutation 

func (s *Spec) HasMutation() bool

HasMutation returns true if the spec mutates any parameter.

func (*Spec) IsFilter 

func (s *Spec) IsFilter() bool

IsFilter returns true if this is a filter-like behavior.

func (*Spec) IsIndexedIterator 

func (s *Spec) IsIndexedIterator() bool

IsIndexedIterator returns true if this spec has an indexed iterator effect.

func (*Spec) IsKeyedIterator 

func (s *Spec) IsKeyedIterator() bool

IsKeyedIterator returns true if this spec has a keyed iterator effect.

func (*Spec) IsSpecInfo 

func (s *Spec) IsSpecInfo()

IsSpecInfo implements typ.SpecInfo.

func (*Spec) IsTableMutator 

func (s *Spec) IsTableMutator() bool

IsTableMutator returns true if this spec has a table mutator effect.

func (*Spec) String 

func (s *Spec) String() string

String returns a string representation.

func (*Spec) WithCallback 

func (s *Spec) WithCallback(paramIdx int, spec *CallbackSpec) *Spec

WithCallback adds a callback specification.

func (*Spec) WithDefaultReturn 

func (s *Spec) WithDefaultReturn(t typ.Type) *Spec

WithDefaultReturn sets the default return when no case matches.

func (*Spec) WithEffectRow 

func (s *Spec) WithEffectRow(row effect.Row) *Spec

WithEffectRow sets the effect row directly.

func (*Spec) WithEffects 

func (s *Spec) WithEffects(labels ...effect.Label) *Spec

WithEffects adds type effects.

func (*Spec) WithEnsures 

func (s *Spec) WithEnsures(constraints ...constraint.Constraint) *Spec

WithEnsures adds postconditions.

func (*Spec) WithExprEnsures 

func (s *Spec) WithExprEnsures(constraints ...constraint.ExprCompare) *Spec

WithExprEnsures adds expression postconditions.

func (*Spec) WithExprRequires 

func (s *Spec) WithExprRequires(constraints ...constraint.ExprCompare) *Spec

WithExprRequires adds expression preconditions.

func (*Spec) WithRequires 

func (s *Spec) WithRequires(constraints ...constraint.Constraint) *Spec

WithRequires adds preconditions.

func (*Spec) WithReturnCase 

func (s *Spec) WithReturnCase(cond constraint.Condition, t typ.Type) *Spec

WithReturnCase adds a conditional return case.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.