Jovial Program Verifier Rugged Jovial Environment.
Final technical rept. 14 Nov 77-15 Nov 81,
SRI INTERNATIONAL MENLO PARK CA
Pagination or Media Count:
This report summarizes project work carried out at the Computer Science Laboratory of SRI International under Contract F30602-78-C-0031 with Rome Air Development Center during the period November 1977 - November 1981. The project has been concerned with the development of a programming environment Rugged Jovial Environment--with verification tools as a principal component--for the specification, development, and formal verification of programs in JOVIAL-J73. The term verification here refers to proof of correctness with respect to formal specification by the method of Floyd assertions. The effort on this project has ranged from fairly abstract work on formal models of computation in particular, regarding the semantics of JOVIAL constructs to practical techniques for implementing these models. This has resulted in the development of a user-friendly system, written in INTERLISP, with the aid of which it is possible to verify JOVIAL software of significant complexity. In addition to our primary project work, we developed several very usefull software tools of more general applicability. These tools are also described in the report.
- Computer Programming and Software
- Computer Systems Management and Standards