Titlebook: International Symposium on Programming; 5th Colloquium, Turi Mariangiola Dezani-Ciancaglini,Ugo Montanari Conference proceedings 1982 Sprin

hermetic

Perluette : A compilers producing system using abstract data types,compilers producing system Perluette. This system is based upon a formal semantics of programming languages. Programming languages are considered to be algebraic data types. Then it becomes possible to specify and prove their implementations as representations of an algebraic data type into another

流利圆滑

PARA

Another characterization of weakest preconditions,e input-output behaviour of programs. These relations include an explicit representation of non-terminating computations. Based on the relational model we introduce a weakest precondition total correctness predicate transformer. We then show how to build up this predicate transformer starting from o

Immunotherapy

Phagocytes

Optimizing for a multiprocessor: Balancing synchronization costs against parallelism in straight-lissor. We adopt a simplified model of a multiprocessor, consisting of several identical processors, all sharing access to a common memory. Synchronization must be done explicitly, using two special operations that take a period of time comparable to the cost of data operations. Our treatment differs

FANG

Intact

Proving the correctness of implementations of shared data abstractions,nsion of Hoare‘s method developed for proving the correctness of an implementation of abstract data types specified in a sequential programming environment. An example is given to illustrate the proposed proof method.

夹死提手势

PUT

Tuning algebraic specifications by type merging,ave the disadvantage of being too much decomposed and hence not directly suited for finding efficient implementations. The paper presents a formal method for overcoming this drawback by combining suitable hierarchical types while simultaneously specifying new (combined) operations.

值得赞赏

An enlarged definition and complete axiomatization of observational congruence of finite processes,gruence ; a finite set of equational axioms is given for the congruence, which we prove to be a complete proof system by argumenting over canonical forms of programs. In a second time, our language is enriched by adding it the necessary operators for expressing the parallel composition of processes