The unified computation laboratory: Modelling, specifications, and tools
Charles Rattray, Robert Graham Clark · Oxford University Press eBooks · 1992
Part 1 Modelling and specification: some mathematical thoughts on languages for data directed design, E. Wagner algebraic alternative for compiler construction, T. Rus algebraic semantics and monad theory, E. Badouel an illustrated mathematical foundation for ERA, C.N.G. Dampney et al on the expressiveness of equational type logic, V. Manca et al linear term rewriting systems are higher dimensional string rewriting systems, M. Johnson inductive reasoning for completing equational software specifications, K.P. Jantke term induction proofs by a generalization of narrowing, U. Fraus and H. Hussmann. Part 2 Formal methods in software development: prototyping and formal specifications, C. Choppy development of modular specifications by stepwise refinements using the PLUSS specification language, M. Bidoit software complexity measures, programming methodologies, and the size of machines, J.C. Cherniavsky and C.H. Smith the implementation of Z specifications using program transformation systems - the SuZan Project, R. Knott and P. Krause the systematic reduction of VDM specifications, A.P. French et al experiences with using formal specification techniques for operations research problems, A.P. French et al a survey of temporal logic methods in system development, N.J. Wilson. Part 3 Specification for communication and concurrency: integrating automata and temporal logic - a framework for specification of real-time systems and software, A. Gabrielian and R. Iyer specification and derivation of process networks, F. Carrez and D. Mery algebraic term nets - a formalism for specifying communications software in the OSI framework, M. Bettaz and A. Choutri using LOTOS in the object-based development of embedded systems, R.G. Clark a data type specification for the process part of basic LOTOS - an axiomatic semantics, G.H.B. Rafsanjani modelling of LOTOS specifications by Petri Nets, G.H.B. Rafsanjani. Part 4 Program verification and development: modules and verification, G. Antoniou program analysis by symbolic execution and generalization, G. Colman et al proving and developing concurrent programs - a small system, D. Mery automated proof and program development, D. Galmiche and O. Hermann interactive automated verification of functional programming languages, R.B. Hughes and R.M. Zimmer theorem proving and program synthesis with Oyster, C. Horn and A. Smaill the PICT system, A.G. Hamilton an interactive tool for deriving correct programs, L. Groves and R. Nickson.