m-Verdi(ID:3951/mve001)
Verdi for m-Eves, precursor of EVES
(m-EVES and EVES were program proving systems, developed for Candian military)
Related languages
References:
Andrews, J.D. "THE m-VERDI EVALUATION REPORT" Andyne Computing Ltd, Kingston ONT (CAN); view details
Abstract: Taken as a whole the m-Verdi is excellent, but it does reveal a few short-commings, which are the subject of this document. These are mostly minor, being weakness of the presentation of the material rather than of the language itself; there are, however, a few points where the language design itself is weak and unclear. Moreover, certain desirable features are missing from the current version of the language and are not, to our knowledge, planned to be included in Verdi.
Craigen, Dan; Kromodimoeljo, Sentot; Meisels, Irwin; Neilson, Andy; Pase, Bill and Saaltink, Mark "m-EVES: A Tool for Verifying Software" view details
Abstract: This paper describes the development of a new tool for formally verifying software. The tool is called m-EVES and consists of a new language, called m-Verdi, for implementing and specifying software; a new logic, which has been proven sound; and a new theorem prover, called m-NEVER, which integrates many state-of-the-art techniques drawn from the theorem proving literature. Two simple examples are used to present the fundamental ideas embodied within the system
Higginson, M.M.; Andrews, J.D. "DISTRIBUTED SYSTEM DESIGN USING MASCOT AND M-VERDI" Andyne Computing Ltd, Kingston ONT (CAN) 15 Jun 1988
view details
Abstract: A Mascot-based design method was developed for real-time distributed computer systems. Mascot, suitably extended, provides a framework for describing, in graphical terms, the separation and dynamic properties of distributed systems. The language used for procedural specifications was m-Verdi. Describes studies done into the feasibility of implementation based on designs developed using the method and on the feasibility of prototyping and simulating designs using the method. Report includes a survey of the literature on formal specifications of distributed systems.
Pase, B.; Kromodimoeljo, S.; Summerskill, K. "PORTING m-EVES TO COMMON LISP" IP Sharp Associates Ltd, Ottawa ONT (CAN) Final Report FR-89-5437-04; 15 Mar 1989
view details
Abstract: m-EVES is a program verification system developed by I.P. Sharp Associates Limited with funding from the Canadian Department of National Defence. m-EVES supports the formal development of mathematical theories and programs written in the m-Verdi language. The main component of the system consists of an interactive theorem prover and an m-ECL interface. A user develops a theory or program interactively by adding declarations to the theorem prover database and directing the theorem prover to perform proofs. The user may also undo declarations, print the status of the database, freeze the state of the database into a file, and thaw the state of the database from a file. The user interacts with m-EVES by using m-ECL (the m-EVES Command Language), which consists of m-Verdi declarations augmented with theorem prover heuristic information, commands to direct the theorem prover to perform proofs, and commands to perform various database operations.
Andrews, J.D. "A Prototype m-Verdi/Ada Environment: A user's manual (Version 1.0)" Andyne Computing Ltd, Kingston ONT (CAN) 28/Sep/1992
view details
Abstract: A user-oriented introduction and tutorial guide to Andyne's prototype m-Verdi/Ada environment. A syntax of the Process Interface Language is provided.
External link: Online copy
Andrews, J.D. "TOWARDS AN M-EVES-BASED FORMAL METHOD FOR M-VERDI/ADA PROCESS NETWORKS" Andyne Computing Ltd, Kingston ONT (CAN) 01 Sep 1992
view details
Abstract: Discusses a developing formal method for a fixed network of process implemented partly in Ada (ARM83) and partly in m-Verdi (Cra87, Saa87). Interprocess communication is based on the remote procedure call model, with processes being organized into clients and servers with respect to any given remotely callable procedure.
External link: Online copy
|