PegaSys and the role of logic in programming environments
The benefits of formal approaches to program development are widely recognized. However, most programming environments have taken little advantage of them. The problem of incorporating formalism into programming environments is discussed in light of two often-competing concerns: maintaining mathematical rigor and alleviating complication in the programming of large systems. The PegaSys system [1,2] represents a practical balance between the two. It deals with an interesting class of program properties that are easy to describe formally and to reason about mechanically. Systems such as PegaSys offer the possibility of increased use of formal methods in programming environments.
KeywordsDecision Procedure Programming Environment Symbolic Execution Control Flow Graph Mathematical Rigor
Unable to display preview. Download preview PDF.
- M. Moriconi and D.F. Hare. The PegaSys system: Pictures as formal documentation of large programs. To appear in ACM Transactions on Programming Languages and Systems.Google Scholar
- M. Moriconi and D.F. Hare. Visualizing program designs through PegaSys. IEEE Computer, 18(8):72–85, August 1985.Google Scholar