Meta-programming with Theory Systems

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.