A FORMAL DESCRIPTION OF VERDI

Authors
  1. Saaltink, M.
Corporate Authors
Odyssey Research Associates Inc, Ottawa ONT (CAN);Chief of Research and Development, Ottawa ONT (CAN) Director of Research and Development Communications and Space
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.
Report Number
TR-89-5429-10 — Technical Report
Date of publication
15 Oct 1989
Number of Pages
80
DSTKIM No
90-04406
CANDIS No
66646
Format(s):
Hardcopy;Originator's fiche received by DSIS

Permanent link

Document 1 of 1

Date modified: