| CAETI Minimal Architecture Specification |
A model of the Minimal Architecture in ACL2 (infix). Includes
extensive pointers to original sources and other
documentation. |
| ACL2 |
ACL2 is
- a logic and programming language in which you can model idgital
systems and
- 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. |
| Executable Z
| 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.
|
| Evaluation Agents |
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.
|
