Safe Haskell	Safe-Inferred
Language	Haskell2010

Copilot.Verifier.Examples.ShouldPass.Structs

Description

An example showing the usage of the What4 backend in copilot-theorem for structs and arrays. Particular focus is on nested structs. For general usage of structs, refer to the general structs example.

Synopsis

data Volts = Volts {
- numVolts :: Field "numVolts" Word16
- flag :: Field "flag" Bool
}
data Battery = Battery {
- temp :: Field "temp" Word16
- volts :: Field "volts" (Array 10 Volts)
- other :: Field "other" (Array 10 (Array 5 Word32))
}
spec :: Spec
verifySpec :: Verbosity -> IO ()

Documentation

data Volts Source #

Definition for Volts.

Constructors

Volts
Fields numVolts :: Field "numVolts" Word16 flag :: Field "flag" Bool

Instances

Instances details

Struct Volts Source #	`Struct` instance for `Volts`.
Instance details Defined in Copilot.Verifier.Examples.ShouldPass.Structs Methods typeName :: Volts -> String # toValues :: Volts -> [Value Volts] # updateField :: Volts -> Value t -> Volts #
Typed Volts Source #	`Volts` instance for `Typed`.
Instance details Defined in Copilot.Verifier.Examples.ShouldPass.Structs Methods typeOf :: Type Volts # simpleType :: Type Volts -> SimpleType #

data Battery Source #

Constructors

Battery
Fields temp :: Field "temp" Word16 volts :: Field "volts" (Array 10 Volts) other :: Field "other" (Array 10 (Array 5 Word32))

Instances

Instances details

Struct Battery Source #	`Battery` instance for `Struct`.
Instance details Defined in Copilot.Verifier.Examples.ShouldPass.Structs Methods typeName :: Battery -> String # toValues :: Battery -> [Value Battery] # updateField :: Battery -> Value t -> Battery #
Typed Battery Source #	`Battery` instance for `Typed`. Note that `undefined` is used as an argument to `Field`. This argument is never used, so `undefined` will never throw an error.
Instance details Defined in Copilot.Verifier.Examples.ShouldPass.Structs Methods typeOf :: Type Battery # simpleType :: Type Battery -> SimpleType #

spec :: Spec Source #

verifySpec :: Verbosity -> IO () Source #