Safe Haskell	Safe-Inferred
Language	Haskell2010

Copilot.Verifier.Examples.ShouldPass.UpdateStruct

Description

An example showing of using copilot-verifier to verify a specification involving structs where individual fields are updated.

Synopsis

Documentation

Definition for Volts.

Constructors

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

Instances details

Struct Volts Source #	`Struct` instance for `Volts`.
Instance details Defined in Copilot.Verifier.Examples.ShouldPass.UpdateStruct 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.UpdateStruct Methods typeOf :: Type Volts # simpleType :: Type Volts -> SimpleType #

Constructors

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

Instances details

Struct Battery Source #	`Battery` instance for `Struct`.
Instance details Defined in Copilot.Verifier.Examples.ShouldPass.UpdateStruct 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.UpdateStruct Methods typeOf :: Type Battery # simpleType :: Type Battery -> SimpleType #