examples

Documentation

Index

• Variables
• func Abs(input int) int
• func Monotone(value float64) float64
• func Retain(lowIn, highIn int) (lowOut, highOut int)
• type Abs_ExecutionModel
• type Retain_ExecutionModel

Variables

var Abs_Contract sopher.AGHyperContract[Abs_ExecutionModel] = sopher.NewAGHyperContract([]sopher.HyperAssertion[Abs_ExecutionModel]{}, []sopher.HyperAssertion[Abs_ExecutionModel]{
	sopher.NewUniversalHyperAssertion[Abs_ExecutionModel](0, 1, sopher.NewPredicateHyperAssertion(func(assignments []Abs_ExecutionModel) bool { e0 := assignments[0]; _ = e0; return e0.ret0 >= 0 })),
	sopher.NewUniversalHyperAssertion[Abs_ExecutionModel](0, 2, sopher.NewPredicateHyperAssertion(func(assignments []Abs_ExecutionModel) bool {
		e0, e1 := assignments[0], assignments[1]
		_, _ = e0, e1
		return !(e0.input >= e1.input) || (e0.ret0 >= e1.ret0)
	}))})

var Retain_Contract sopher.AGHyperContract[Retain_ExecutionModel] = sopher.NewAGHyperContract(
	[]sopher.HyperAssertion[Retain_ExecutionModel]{},
	[]sopher.HyperAssertion[Retain_ExecutionModel]{sopher.NewUniversalHyperAssertion[Retain_ExecutionModel](0, 2, sopher.NewPredicateHyperAssertion(func(assignments []Retain_ExecutionModel) bool {
		e0, e1 := assignments[0], assignments[1]
		_, _ = e0, e1
		return !(e0.highIn == e1.highIn) || (e0.lowOut == e1.lowOut)
	}))})

Functions

func Abs

func Abs(input int) int

guarantee: forall e0. e0.ret0 >= 0 guarantee: forall e0 e1. !(e0.input >= e1.input) || (e0.ret0 >= e1.ret0)

func Monotone

func Monotone(value float64) float64

assume: forall e. e.value >= 0 && e.value <= 100_000 guarantee: forall e0 e1. e0.value >= e1.value; <-> e0.ret0 >= e1.ret0

func Retain

func Retain(lowIn, highIn int) (lowOut, highOut int)

guarantee: forall e0 e1. !(e0.highIn == e1.highIn) || (e0.lowOut == e1.lowOut)

Types

type Abs_ExecutionModel

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

type Retain_ExecutionModel

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