A theory system is a collection of interdependent theories, some if which stand in a meta/object relationship, forming an arbitrary num­ber of meta­levels. The main thesis of this chapter is that theory systems constitute a suitable formalism for constructing advanced ap­plications in reasoning and software engineering. The Alloy language for defining theory systems is introduced, its syntax is defined and a collection of inference rules is presented. A number of problems suit­able for theory systems are discussed, with program examples given in Alloy. Some current implementation issues and future extensions are discussed.

Publisher  MIT Press
All copyrights reserved by MIT Press 2007.

Details

Previous Versions

Jonas Barklund, Katrin Boberg, Pierangelo Dell'Acqua, and Margus Veanes. Meta-programming with Theory Systems, May 1995.