Verdi(ID:2606/ver001)

for the Italian composer Giuseppe Verdi

Provable systems language. Descendant of Ottawa Euclid.
Related languages
m-Verdi => Verdi   Evolution of
Verdi => SPARC Verdi   Implementation
Verdi => s-Verdi   Extension of
References:
  • Saaltink, M. "A FORMAL DESCRIPTION OF VERDI" Odyssey Research Associates Inc, Ottawa ONT (CAN) Technical Report TR-89-5429-10; 15 Oct 1989 view details Abstract: Verdi is a notation for expressing programs and their specifications. The present report gives a precise formal description of Verdi (to the level of abstract syntax) and defines the proof obligations that must be proved to demonstrate that a program is in consonance with its specifications. A model theory (semantics) of the language is defined and used to show the adequacy of the proof obligations.
  • Craigen, D. "REFERENCE MANUAL FOR THE LANGUAGE VERDI" Odyssey Research Associates Inc, Ottawa ONT (CAN) Technical Report TR-90-5429-09; 15 Feb 1990 view details Abstract: The document presents an informal description of the language Verdi. Verdi is the interface language with the EVES (Version 1.0) verification system and consists of components for specifying and implementing programs, for proving consistency between specification and implementations, and for supporting miscellaneous other system capabilities.
  • Saaltink, M.; Craigen, D. "SIMPLE TYPE THEORY IN EVES" Odyssey Research Associates Inc, Ottawa ONT (CAN) 01 Jan 1990 view details Abstract: The paper presents a brief description of a newly completed verification system called EVES. EVES is a formal system based on Zermelo-Fraenkel set theory with the Axiom of Choice. EVES supports the proof of mathematical properties, including proofs of program correctness. The development of EVES required the design of a new language, called Verdi, and of a heuristic theorem prover, called NEVER. After introductory remarks on Verdi, NEVER and EVES, we present a combinatory version of Church's simple type theory in EVES as an illustration of the power and flexibility of the untyped set theory framework and of EVES.
  • D. Craigen, S. Kromodimoeljo, I. Meisels, W. Pase and M. Saaltink. "EVES: An Overview" In "Proceedings of VDM '91 (Formal Software Development Methods)", Noordwijkerhout, The Netherlands (October 1991), Lecture Notes in Computer Science 551, Springer-Verlag, Berlin, 1991. view details Abstract: In this paper we describe a new formal methods tool called EVES. EVES consists of a set theoretic language, called Verdi, and an automated deduction system, called NEVER. We present an overview of Verdi, NEVER, and the underlying mathematics; and develop a small program, to demonstrate the basic functionality of EVES. Previously CP-91-5402-43.
  • Irwin Meisels "Verdi Interpreter User's Manual" ORA Canada, April 1991 view details ps Abstract: This document describes the interpreter component of the EVES program verification system. Most of this report has been incorporated into the Verdi Reference Manual.
  • D. Craigen, S. Kromodimoeljo, I. Meisels, B. Pase and M. Saaltink. "EVES System Description" In Proceedings of CADE-11, Saratoga Springs, NY (June 1992), Springer-Verlag, New York, 1992. view details Abstract: A brief description of the Verdi language, concentrating on the EVES verification environment that has been implemented, particularly the theorem prover component.
  • Mark Saaltink, Sentot Kromodimoeljo, Bill Pase, Dan Craigen and Irwin Meisels "An EVES Data Abstraction Example" In Proceedings of "Formal Methods Europe'93" (FME'93, Odense, Denmark), Springer-Verlag, April 1993. view details Abstract: This paper provides an introduction to EVES. EVES is a formal methods tool consisting of a language based on set theory, called Verdi, and an automated deduction system, called NEVER. We provide a general introduction to EVES and demonstrate its capabilities using an example of data abstraction (table/list).
  • Irwin Meisels "Translating Verdi Intermediate Language into SPARC Code" ORA Canada, July 1994. view details Abstract: This paper specifies the translation of Verdi intermediate language (IL) into code for the SPARC architecture. The IL in this document is an abstract version of the IL described in Structure of the SPARC Verdi Compiler, in which no distinction is made between operator attributes and operands.
  • Meisels, Irwin An Alternative Syntax for Verdi. ORA Technical Report TR-94-5478-02, March 1994. view details Abstract: This document describes an alternative syntax for Verdi. The design for this syntax had the following goals: the new syntax should be closer to what people are used to (Pascal or Ada-like declarations and infix expression syntax); the new syntax should be easily transliterated into Verdi syntax, and vice versa; and the new expression syntax should be flexible. This document presents the lexical and syntactic structure of the new syntax, and shows how the transliteration to Verdi is done. ps