ST package:sbv
Symbolic version of the type
T.
The state of the symbolic interpreter
Equivalent to Haskell's chr
Check if string is in the regular expression
Retrieve string encoded by integer i (ground rewriting only)
Retrieve integer encoded by string s (ground rewriting only)
Equivalent to Haskell's ord
Implementation of full-binary symbolic trees, providing logarithmic
time access to elements. Both reads and writes are supported.
A symbolic tree containing values of type e, indexed by elements of
type i. Note that these are full-trees, and their their shapes remain
constant. There is no API provided that can change the shape of the
tree. These structures are useful when dealing with data-structures
that are indexed with symbolic values where access time is important.
STree structures provide logarithmic time reads and writes.
A stability condition captures a primary input that does not change.
Use
stable to create elements of this type.
Are we in a good state, or in a stuck state?
A statement in our imperative program, parameterized over the state.
Execution got stuck, with the failing VC
AES state. The state consists of four 32-bit words, each of which is
in turn treated as four GF28's, i.e., 4 bytes. The T-Box
implementation keeps the four-bytes together for efficient
representation.
Each agent can be in one of the three states