摘要：

this report. Dan Craigen reviewed the report at various stages. iv EVES Project TR-90-5446-02 Chapter 1 Introduction A model theory and (parts of) a logic for Verdi are presented in the formal description of Verdi [12], together with a proof of soundness for the logic with respect to the model theory. While this development was useful in validating the proof theory, certain aspects of the model theory are unsatisfactory. In particular, the model-theoretic semantics is highlyit is unclear exactly how certain parts of Verdi would be implemented. The present work complements the model theory by presenting an alternative definition of the semantics of the executable portion of Verdi, with a proof of correspondence between the new semantics and the old. The new semantic definition is denotational in style [4, 13, 14]. I tried as much as possible, within the other constraints of the project, to adopt the so-called "standard" style of definition. However, I avoided many of the usual typographical and notational conventions, as these were inconsistent with the existing model theory. Since the bulk of this report describes the relationship between the two definitions, notational inconsistencies are both awkward and annoying. Particular conventions avoided include "currying" of the semantic functions, the use of juxtaposition to indicate application, and semantic parentheses surrounding program text. Various aspects of Verdi are explained by the new semantic definition. In particular, there were a number of design considerations that, while significant to any implementor of the language, are not apparent in the model theory. Among these considerations are

展开