No abstract available.

Synthesis and verification of systems with finite state space are well established problems in logic and computer science and have a long history. Precise formulations are based on preliminary formalization of two languages: SPEC (for specifications), IMP (for implementations) and a (satisfaction) relation, sat, included in IMP x SPEC. Clearly, one can consider different languages which may reflect a variety of abstraction levels. It may well happen that an object at a given level may serve as implementation for a higher level and also as specification for a lower level. From this perspective the three level paradigm is instructive and there is a proliferation of its versions. Though many of them are relevant to the subject, in this lecture the author singles out only one to which he refers to as The Trinity, namely: at the highest level-specifications expressed as formulas based on second order monadic logic (SOML); at the intermediate level-formalization of transducers (i.e. transformers of input signals into output signals) via finite sequential automata; at the lower level-formalization of discrete synchronous hardware via logical nets.

this paper most relevant is a series of publications by Gries, Ovicki, Nguyen, Demers, Schneider, Widom, Panangaden (see the list of references). We refer to this series as to [GONDSWP], the favorite references being [WGS1] and [WGS2], where additional bibliographical information can be found. The important contribution of [GONDSWP] is that in addition to the compositionality paradigm promoted in [MC], they address systematically the crucial issue of completeness for the proposed proof rules. A comprehensive and critical analysis of [GONDSWP] is given in N. Soundararajan's re1

The authors investigate and compare two ways of specifying stream relations (in particular, stream functions). The first uses relational programs, i.e., netlike program schemes in which the signature primitives are interpreted as relations over a given CPO. No stream domains are assumed; semantics is in fixed-point style. The second is through data flow nets, i.e., nets whose nodes are interpreted as processes (computational stations). The authors prove the existence of an adequate data flow interpreter for relational programs over all relations and its uniqueness. When dealing with functions the interpreter is modular and obeys the Kahn principle, the authors identify two kinds of anomalies. The first (meagerness anomaly) is caused by the defect of the used processes (computational stations) and holds in fact for arbitrary input-output behaviors. The second (ambiguity anomaly) is rooted in the semantics of relational nets over arbitrary CPO. It is unavoidable in any extension beyond functional behaviors.>

Denotational semantics for an ALGOL-like language with finite-mode procedures, blocks with local storage, and sharing (aliasing) is given by translating programs into an appropriately typed l-calculus. Procedures are entirely explained at a purely functional level - independent of the interpretation of program constructs - by continuous models for l-calculus. However, the usual (cpo) models are not adequate to model local storage allocation for blocks because storage overflow presents an apparent discontinuity. New domains of store models are offered to solve this problem.