language

package
v0.0.0-...-df44091 Latest Latest
Warning

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

 Go to latest Published: Nov 14, 2024 License: MIT Imports: 17 Imported by: 0

Documentation

Index

Constants

View Source 
const (
	LiftedFalse   = LiftedBoolean(0b0000)
	LiftedUnknown = LiftedBoolean(0b0001)
	LiftedTrue    = LiftedBoolean(0b0011)
)
View Source 
const (
	RegionToken = TokenClass(iota)
	ForallToken
	ExistsToken
	AssumeToken
	GuaranteeToken
	IdentifierToken
	ProbabilityToken
	ExpressionToken
	ScopeDelimiterToken
	ExpressionDelimiterToken
	LeftParenthesis
	RightParenthesis
	EofToken
)

Variables

View Source 
var ErrFileNotFound = errors.New("file could not be found")

Functions

func LexDocStrings 

func LexDocStrings(docs []string) iter.Seq[Token]

func LexGo 

func LexGo(comments *ast.CommentGroup) iter.Seq[Token]

func LexRunes 

func LexRunes(runes []rune) iter.Seq[Token]

func LexString 

func LexString(str string) iter.Seq[Token]

func Print 

func Print(ast Node) string

Types

type AGHyperContract 

type AGHyperContract[T any] struct {
	// contains filtered or unexported fields
}

func NewAGHyperContract 

func NewAGHyperContract[T any](
	assumptions, guarantees []HyperAssertion[T],
) AGHyperContract[T]

func (*AGHyperContract[T]) Assume 

func (contract *AGHyperContract[T]) Assume(executions ...T) LiftedBoolean

func (*AGHyperContract[T]) Guarantee 

func (contract *AGHyperContract[T]) Guarantee(executions ...T) LiftedBoolean

func (*AGHyperContract[T]) Model 

func (contract *AGHyperContract[T]) Model(call func(input T) T)

type Assumption 

type Assumption struct {
	// contains filtered or unexported fields
}

func NewAssumption 

func NewAssumption(assertion Node) Assumption

type ConditionalProbabilityQuantifier 

type ConditionalProbabilityQuantifier struct {
	// contains filtered or unexported fields
}

func NewConditionalProbabilityQuantifier 

func NewConditionalProbabilityQuantifier(event, given Node) ConditionalProbabilityQuantifier

type ConstantNumber 

type ConstantNumber struct {
	// contains filtered or unexported fields
}

func Number 

func Number(value float32) ConstantNumber

type Contract 

type Contract struct {
	// contains filtered or unexported fields
}

func NewContract 

func NewContract(regions ...Region) Contract

type Existential 

type Existential struct {
	// contains filtered or unexported fields
}

func NewExistential 

func NewExistential(variables []string, assertion Node) Existential

type ExistentialHyperAssertion 

type ExistentialHyperAssertion[T any] struct {
	// contains filtered or unexported fields
}

func NewExistentialHyperAssertion 

func NewExistentialHyperAssertion[T any](offset, size int, body HyperAssertion[T]) *ExistentialHyperAssertion[T]

func (ExistentialHyperAssertion[T]) Accept 

func (assertion ExistentialHyperAssertion[T]) Accept(visitor HyperAssertionVisitor[T])

func (ExistentialHyperAssertion[T]) Size 

func (assertion ExistentialHyperAssertion[T]) Size() int

type Files 

type Files struct {
	// contains filtered or unexported fields
}

func NewFiles 

func NewFiles() Files

func (*Files) Add 

func (files *Files) Add(path string) error

func (*Files) AddDirectory 

func (files *Files) AddDirectory(path string) (err error)

func (*Files) AddFile 

func (files *Files) AddFile(path string) error

func (*Files) Iterator 

func (files *Files) Iterator() iter.Seq[string]

type GoExpresion 

type GoExpresion struct {
	// contains filtered or unexported fields
}

func NewGoExpression 

func NewGoExpression(code string) GoExpresion

type Group 

type Group struct {
	// contains filtered or unexported fields
}

func NewGroup 

func NewGroup(node Node) Group

type Guarantee 

type Guarantee struct {
	// contains filtered or unexported fields
}

func NewGuarantee 

func NewGuarantee(assertion Node) Guarantee

type HyperAssertion 

type HyperAssertion[T any] interface {
	Accept(visitor HyperAssertionVisitor[T])
	Size() int
}

HyperAssertion represents an interface for tracking and evaluating the state of assignments over a sequence of elements, typically in the context of quantifiers in formal verification or monitoring systems.

func HyperAssertionFromAST 

func HyperAssertionFromAST[T any](node Node) HyperAssertion[T]

type HyperAssertionInterpreter 

type HyperAssertionInterpreter[T any] struct {
	// contains filtered or unexported fields
}

func NewHyperAssertionInterpreter 

func NewHyperAssertionInterpreter[T any]() HyperAssertionInterpreter[T]

func (*HyperAssertionInterpreter[T]) ExistentialHyperAssertion 

func (interpreter *HyperAssertionInterpreter[T]) ExistentialHyperAssertion(assertion ExistentialHyperAssertion[T])

func (*HyperAssertionInterpreter[T]) PredicateHyperAssertion 

func (interpreter *HyperAssertionInterpreter[T]) PredicateHyperAssertion(assertion PredicateHyperAssertion[T])

func (*HyperAssertionInterpreter[T]) Satisfies 

func (interpreter *HyperAssertionInterpreter[T]) Satisfies(assertion HyperAssertion[T], elements []T) bool

func (*HyperAssertionInterpreter[T]) TrueHyperAssertion 

func (interpreter *HyperAssertionInterpreter[T]) TrueHyperAssertion(assertion TrueHyperAssertion[T])

func (*HyperAssertionInterpreter[T]) UniversalHyperAssertion 

func (interpreter *HyperAssertionInterpreter[T]) UniversalHyperAssertion(assertion UniversalHyperAssertion[T])

type HyperAssertionVisitor 

type HyperAssertionVisitor[T any] interface {
	UniversalHyperAssertion(assertion UniversalHyperAssertion[T])
	ExistentialHyperAssertion(assertion ExistentialHyperAssertion[T])
	PredicateHyperAssertion(assertion PredicateHyperAssertion[T])
	TrueHyperAssertion(assertion TrueHyperAssertion[T])
}

type Injector 

type Injector struct{}

func NewGoInjector 

func NewGoInjector() Injector

func (Injector) CallWrap 

func (injector Injector) CallWrap(function *dst.FuncDecl) *dst.AssignStmt

func (Injector) Check 

func (injector Injector) Check(name string, contractName string) *dst.IfStmt

func (Injector) ConstructModel 

func (injector Injector) ConstructModel(model string, function *dst.FuncDecl) *dst.AssignStmt

func (Injector) Contract 

func (injector Injector) Contract(model string, function *dst.FuncDecl) (string, *dst.GenDecl)

func (Injector) Files 

func (injector Injector) Files(files iter.Seq[string])

func (Injector) HasNamedOutputs 

func (injector Injector) HasNamedOutputs(function *dst.FuncDecl) bool

func (Injector) Imports 

func (injector Injector) Imports(file *dst.File, imports map[string]string)

func (Injector) Inject 

func (injector Injector) Inject(file *dst.File)

func (Injector) InputFields 

func (injector Injector) InputFields(function *dst.FuncDecl) (fields []*dst.Field)

func (Injector) Model 

func (injector Injector) Model(function *dst.FuncDecl) (string, *dst.GenDecl)

func (Injector) OutputFields 

func (injector Injector) OutputFields(function *dst.FuncDecl) (fields []*dst.Field)

func (Injector) Restore 

func (injector Injector) Restore(files iter.Seq[string])

func (Injector) Return 

func (injector Injector) Return(function *dst.FuncDecl) *dst.ReturnStmt

func (Injector) Updates 

func (injector Injector) Updates(function *dst.FuncDecl) (updates []*dst.AssignStmt)

func (Injector) Wrap 

func (injector Injector) Wrap(function *dst.FuncDecl) *dst.AssignStmt

type Lexer 

type Lexer struct {
	// contains filtered or unexported fields
}

func NewLexer 

func NewLexer(runes iter.Seq[rune]) Lexer

func (*Lexer) Scan 

func (lexer *Lexer) Scan() iter.Seq[Token]

type LiftedBoolean 

type LiftedBoolean uint8

func LiftBoolean 

func LiftBoolean(value bool) LiftedBoolean

func (LiftedBoolean) And 

func (lhs LiftedBoolean) And(rhs LiftedBoolean) LiftedBoolean

func (LiftedBoolean) IsFalse 

func (boolean LiftedBoolean) IsFalse() bool

func (LiftedBoolean) IsTrue 

func (boolean LiftedBoolean) IsTrue() bool

func (LiftedBoolean) IsUnknown 

func (boolean LiftedBoolean) IsUnknown() bool

func (LiftedBoolean) Not 

func (boolean LiftedBoolean) Not() LiftedBoolean

func (LiftedBoolean) Or 

func (lhs LiftedBoolean) Or(rhs LiftedBoolean) LiftedBoolean

func (LiftedBoolean) String 

func (boolean LiftedBoolean) String() string

type MonitorFactory 

type MonitorFactory struct {
	// contains filtered or unexported fields
}

func NewGoMonitorFactory 

func NewGoMonitorFactory(packageName, modelName string) MonitorFactory

func (*MonitorFactory) Create 

func (factory *MonitorFactory) Create(node Node) *dst.CallExpr

func (*MonitorFactory) NewExistentialMonitorCall 

func (factory *MonitorFactory) NewExistentialMonitorCall(existential Existential) *dst.CallExpr

func (*MonitorFactory) NewPredicateMonitorCall 

func (factory *MonitorFactory) NewPredicateMonitorCall(expression GoExpresion) *dst.CallExpr

func (*MonitorFactory) NewUniversalMonitorCall 

func (factory *MonitorFactory) NewUniversalMonitorCall(universal Universal) *dst.CallExpr

type Node 

type Node interface{}

type Parser 

type Parser struct {
	// contains filtered or unexported fields
}

func NewParser 

func NewParser(tokens iter.Seq[Token]) Parser

func (*Parser) Parse 

func (parser *Parser) Parse() Contract

type PredicateExpression 

type PredicateExpression[T any] struct {
	// contains filtered or unexported fields
}

func NewPredicateExpression 

func NewPredicateExpression[T any](predicate func(assignments []T) bool) PredicateExpression[T]

type PredicateHyperAssertion 

type PredicateHyperAssertion[T any] struct {
	// contains filtered or unexported fields
}

func NewPredicateHyperAssertion 

func NewPredicateHyperAssertion[T any](predicate func(assignments []T) bool) *PredicateHyperAssertion[T]

func (PredicateHyperAssertion[T]) Accept 

func (assertion PredicateHyperAssertion[T]) Accept(visitor HyperAssertionVisitor[T])

func (PredicateHyperAssertion[T]) Size 

func (assertion PredicateHyperAssertion[T]) Size() int

type ProbabilisticQuantifier 

type ProbabilisticQuantifier struct {
	// contains filtered or unexported fields
}

func NewProbabilisticQuantifier 

func NewProbabilisticQuantifier(body Node) ProbabilisticQuantifier

type Region 

type Region struct {
	// contains filtered or unexported fields
}

func NewRegion 

func NewRegion(name []string, assumptions, guarantees []Node) Region

type Token 

type Token struct {
	// contains filtered or unexported fields
}

func NewToken 

func NewToken(class TokenClass, lexeme string) Token

type TokenClass 

type TokenClass uint8

func (TokenClass) String 

func (class TokenClass) String() string

type TrueHyperAssertion 

type TrueHyperAssertion[T any] struct{}

func NewTrueHyperAssertion 

func NewTrueHyperAssertion[T any]() *TrueHyperAssertion[T]

func (TrueHyperAssertion[T]) Accept 

func (assertion TrueHyperAssertion[T]) Accept(visitor HyperAssertionVisitor[T])

func (TrueHyperAssertion[T]) Size 

func (assertion TrueHyperAssertion[T]) Size() int

type Universal 

type Universal struct {
	// contains filtered or unexported fields
}

func NewUniversal 

func NewUniversal(variables []string, assertion Node) Universal

type UniversalHyperAssertion 

type UniversalHyperAssertion[T any] struct {
	// contains filtered or unexported fields
}

func NewUniversalHyperAssertion 

func NewUniversalHyperAssertion[T any](offset, size int, body HyperAssertion[T]) *UniversalHyperAssertion[T]

func (UniversalHyperAssertion[T]) Accept 

func (assertion UniversalHyperAssertion[T]) Accept(visitor HyperAssertionVisitor[T])

func (UniversalHyperAssertion[T]) Size 

func (assertion UniversalHyperAssertion[T]) Size() int

Source Files

View all Source files

Directories

Path Synopsis
example
sub

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.