|CAETI Minimal Architecture Specification
||A model of the Minimal Architecture in ACL2 (infix). Includes
extensive pointers to original sources and other
- a logic and programming language in which you can model idgital
- a tool to help you prove properties of those models.
|Infix interface for
ACL2||For those uncomfortable with the Lisp syntax of ACL2,
we provide a more conventional infix interface in which guards
appear as conventional types. We argue that this logic should be
easily adoptable by software engineers, in contrast to other
non-constructive, formal systems such as Z or PVS.|
||EZ provides a capability to parse an extended Z file,
and generate executable functions corresponding to state changing schema.
The subset of Z that we support includes globals, axioms,
schemas and types.
||An example of a real-time evaluation agent in the MOO. In this
case it tracks a finite state model of the events involving the
student. More generally, such evaluation agents could be used to track
adherence of a system to its formal specification. The finite
state model allows us to check temporal properties.