412 Pages

1982

9.676 MB

English

Most books are stored in the elastic cloud where traffic is expensive. For this reason, we have a limit on daily download.

Lecture Notes ni retupmoC ecneicS detidE yb .G Goos dna .J sinamtraH 731 III II I II I lanoitanretnI muisopmyS no gnimmargorP ht5 muiuqolloC ,niruT April 6-8, 2891 sgnideecorP detidE yb .M inilgacnaiC-inazeD dna .U iranatnoM galreV-regnirpS Berlin Heidelberg NewYork 1982 Editorial Board W. Brauer .P Brinch Hansen .D Gries C. Meier .G SeegmLiller .J Steer .N Wirth Editors Mariangiola Dezani-Ciancaglini ISI C.so M.D'Azeglio 42, Torino, italy 10125 Ugo Montanari ISI C.so Italia 40, 56100 Pisa, Italy AMS Subject Classification (1980): 68 05, B 68 B ,01 68 B 20 CR Subject Classification :)1891( 4.20, 5.24 ISBN Springer-Verlag 3-540-11494-7 Berlin Heidelberg New York ISBN 0-387-11494-? Springer-Verlag New York Heidelberg Berlin This work is subject to copyright. All rights are reserved, whether the whoolre part of the material is concerned, specifically thoseo f translatiorne,p rinting, re-use of illustrations, broadcasting, reproduction by photocopying machine or similar means, and storage in data banks. Under 3£ 54 of the German Copyright Law where copies are made for other than private use, a fee is payable to "Verwertungsgesellschaft Wort", Munich. © by Spdnger-Verlag Bedin Heidelberg 1982 Printed in Germany Printing and binding: BeltzO ffsetdruck, Hemsbach/Bergstr. 2145/3140-543210 FOREWORD The 25 papers contained in this volume have been selected among 75 sub- n~itt~ papers for presentation at the V-th International Symposium on Programming (Toriho, April 6-8, 1982). The previus four colloquia were held in Paris in 1974, 76, 78 and 80. The Program Committee consisted of J.ARSAC, Universit~ P.et M.Curie, Paris; G.AUSIELLO, Universit~ di Roma; M.DEZANI, Universit~ di Torino; P.HENDERSON, Oxford University; C.GIRAULT, Universit~ P. et M.Curie, Paris; D.GRIES, Cornell University, Ithaca (NY); A.MARTELLI, Univer- sit~ di Torino; U°MONTANARI (Chairman), Universit~ di Pisa; M.NIVAT, Universit~ Paris ,7 Paris; M.PAUL, Technische Universit~t, Munich; B.ROBINET, Universit~ .P et M.Curie, Paris; M.SINTZOFF, Mble Research Laboratory, Bruxelles. The Organizing Committee consisted of l.Margaria, S.Ronchi della Roeca, F.Sirovich, M.Zacchi, Istituto di Seienze dell'Informazione, Torino. The editors feel very grateful to the other members of the Program Committee and to the following referees:L.Aiello, A°Albani, V.Ambriola, P.Ancillotti, A°Arnold, E.Astesiano, F.Baiardi, R°Barbuti, H.Barendregt, M.Bellia, J.Berstel, O.Carvalho, P.Chretienne, M.Coppo, P.Degano, G.De Miehelis, R.De Mori, S.Eiehhole, K.Elhardt, M.Fontet, H~Ganzinger, G.Gardarin, M.C.Gaudel, R.Giegerich, R.Gnatz, F.Grandoni, PoGreussay, J.Guessarian, G.Guiho, C.Herzog, B.Hoferer, W.Lahner, G.Levi, G.Longo, B.Lorho, H.Lovenieh, F.Luccio, A°Maggiolo-Sehettini, D.Mandrioli, .I Margaria, M.Martelli, G.Maurl, P.Miglioli, C.Montangero, L.Nolin, M. Ornaghi, G.Pacini, H.Partsch, P.Pepper, J.F.Perrot, A.Pettorossi, G.Pujone, V.von Rhein, G.Roncairol, S.Ronchi, E.Saint-James, P.SalI~, III M.Simi, F.Sirovich~ M.Somalvieo, P.G.Terrat, F.Turini, G.Vaglini, M. Vanneschi, BoVenneri, M.Venturini-Zilli, H.Vogel, A.Widery, M.Wirsing, M.Zacchio Moreover we acknowledge the financial support provided by the follo- wing institutions and firms: C.N.R. - Comitato per le 5cienze Matematiche C.N~R. - G.N.A~S~I,!o C,N.Ro - Progetto Finalizzato Informatica - 0biettivo CNET - Unit~ ISI Pisa e Torino~ Cassa di Risparmio di Torlno Comune di Torino Regione Piemonte = Assessorato alla Cultura Olivetti S.p,A~ AoI.C.A. Mariangiola Dezani~ Ciancaglini Ugo Montanar i IstiKuto di Scienze Llnfodremlalz ione Istituto di Scienze dell'Informazione Universitg di Torino Universitg di Pisa V! M.Rk~!A, E.DAMERI, P.DEC~NO,G.LEVI, M . ~ I Applicative ccmmunicating processes in first order logic ........................ 1 • B D. B~qSON A mchine level semantics for nondete~ninistic, parallel programs .... .......... . 15 J.A. B~RSSTRA, J.W. KLOP A formalized proof system for total correctness of while programs ............... 26 E. OOSTA Autcmatic prcgran transformation viewed as theorem proving ...................... 37 P. DARONDFAU An enlarged definition and ccmplete axicmatization of observational congruence of finite processes ................................................................ 47 P PM12P2q.ED. Perluette: A compilers producing system using abstract data types ............... 63 T.ELRAD, N.FRANCEZ A weakest precondition semantics for gnitacintarsrcc processes .................. 78 P. ~MAhTJ~SON Frcm abstract model to efficient ccrmpilation of patterns ........................ 91 ~.ERIKSSON, A. JOHANSSON Ccmputer-based synthesis of logic programs ...................................... 105 M.P.FLE, G. ROUCAIROL On scme syntactic equivalence of program schemas and related transformations .... 116 R.~, W.P.DE RoarER, M.RONCKEN Procedures and concurrency: A study in proof ..................................... 132 P.GUERREIR0 Another characterization of weakest preconditions ................. .............. 164 V M.C.B.~Y Powerdcmains and nondeterministic recursive definitions ......................... 178 .p G. HrRPm/~D, T.L. RODI~EFFER Optimizing for a ~itiprocessor: Balancing synchronization costs against parallelism in straight-ILne code ........................................................... 194 R. HINDLEY The simple s~aantics for Coppo-Dezani - Sall~ types ............................. 212 L. KOZMA Proving the correctness of ir~ples~ntatiors of shared data abstractions ............ 227 .P JORRAND Specification of conTm/nicating processes and process imple~entation correctness. 242 J. LF~ZCZYLOWSKI, M. WIRSING A system for reasoning within and about algebraic specifications ................ 257 A.LAUT, H. PAI~SCH Tuning algebraic specifications by type merging ................................. 283 A. ~I~OSSI, A. q~f~WOKS Cc~m/nicating agents for applicative concurrent progranmling ..................... 305 A. POIGNE' On effective ccmputations of nondeterministic schemes ........................... 323 J.P.QUEII/~, J. SIFAKIS Specification and verification of concurrent systems in CESAR ................... 337 J. M. RUSHBY Prcof of separability. A verification technique for a class of a security kernels352 M. SZOTS, .S CSIZMAZIA A method for progr~ synthesis.- ................................................ 368 J.A. TOWNLEY The use of transformations to i~plement an algorithm ............................ 381 IV APPLICATIVE COMM~CAI'H~I(; SESSECORP IN TSRIF REDRO CIGOL Marco Bellia, Pierpaolo Degano and Giorgio Levi tstituto di Scienze dell'Informazione Universit~ di Pisa, Italy Enrico Dameri Systems & Management SpA, Area Tecnologie Software Pisa, Italy Maurizio Martelti Istituto CNUCE - C.N.R., Pisa, Italy TCARTSBA eW ebircsed a first applicative order egaugnal for eht specification of deterministic smetsys of communicating computing stnega ~ aI .neeuQcaM-nhaK Both the sequential dna parallel interpreter we give are based on lazy evaluation, are demand driven and can handle infinite streams and non-terminating procedures. An equivalent least fixed-point semantics is then presented which neatly copes with the above features of the language, tt is worth noting that computations in our logical based model can be considered as format proofs, thus making format reasoning about programs easier. L INTRODUCTION The aim of this paper is to give a model of distributed computing based on an applicative fir'st order logic language. The communicating computing agents we describe are essentially those modelled by Kahn and MacGlueen /12, 13/, i.e. processes whose data are streams and which exchange information through one-way (single writer and multiple readers) channels. Since we want our language to be applicative, the agents we model are stateless, and the basic computation step consists in a reconfiguration of a system of computin 9 agents (SCA). The language we propose is a modification of PROLOG /14/. Any SCA is modelled by a set of atomic formulas, each corresponding to a single agent. Distributed programs are detneserper as sets of procedurally interpreted Horn clauses, each being a process definition. Channels which connect two or more agents ere modelled by the presence of the same variabte in the corresponding atomic formulas, tn order to limit ourselves to statically defined one-way channels, we restrict PROLOG by staticalty distinguishing the input arguments of an atomic formula from its output arguments. This restriction to PROLOG limits its expressive power as far as problem solving is concerned, e.g. it forbids invertibility. On the other hand, PROLOG has been extended to cope with infinite streams, which require our language to have non-strict processes and lazy constructors. In spite of the above outlined modifications, the simple and clear logical concepts which underly PROLOG need to be only slightly modified to provide a fixed-point semantics of our language. Remarkably enough, the semantics is defined in terms of a least fixed-point construction, even in the presence of non-terminating processes. Finally~ let us note that our language can be seen as a proper extension of term rewriting systems~ when Horn clauses are interpreted as rewrite rules extended to provide more than one output. Thus, we argue that relevant properties and proof techniques of term rewriting systems~ such as Church-Rosser property and Knuth-Bendix completion algorithm, can be generalized and used here. In Sections 2 and 3 we will introduce the syntax of the language we use to talk about agents and channels. Then~ we will discuss the behaviour of SCA's in terms of lazy system transformations. Finally~ we will define a fixed-point semantics~ related to the model theoretic semantics of logic theories. 2. BASIC SYNTACTIC CONSTRUCTS Our language is a many sorted first order language~ which allows to express the behaviour of SCA's in terms of rewriting systems. The language alphabet is ~= {S, C~ D, ~V F~ R} , where: S]s a set of identifiers. Given S, we define a sort s which is: i) simple if s E S, ii) funetional if s E S~--~S, iii) relational if s E S~--~S *. C is a family of sets of constant symbols indexed by simple sorts. D is a family of sets of data constructor symbols indexed by functional sorts. V is a family of denumerable sets of variable symbols indexed by simple sorts. F is a family of sets of function symbols indexed by functionaI sorts. R s~ a family of sets of pEedieate symbols indexed by relational sorts. The basic eon~tr'uct of the language is the atomic formula~ with corresponds to the agent~ the basic component of a SCA. An atomic formula is: i) a data atomic formula of the form d(tl,...,tm)=V, such that tz,...,t m are data terms of sorts sz,..,Sm~ v is a variable symbol of sort s and dED has sort I s x ... x Sm---~ s, or ii) a functional atomic formula of the form f(tzg...~tm)=V~ such that tl,...,t m are data terms of sorts Sl,...~Sm~ v is a variable symbol of sort s and feF has sort I s x ... x Sm---~ ~s or iii) a relational atomic formula of the form r(in, tl,..~tm;OUt: Vm+l,...~Vn)~ such that tl,...~t m are data terms of sorts sl~...,Sm~ Vm+l~...~v n are variable symbols of sorts Sm+l,..,s n and rE R has sort I s x ... x Sm--~ Sm+ 1 x ... x s n. A data term of sort s (sES) is: i) a constant symbol of sort s, ii) a variable symbol of sort s, iii) a data constructor application d(tl,..,t m) such that t],...~t m are data terms of sorts Sl~...~s m and d D E has sort 1 s x ... x Sm---.~ s. A system formula (s-formula) is either: i) an atomic formula, or ii) a formula of the form Cl,C 2 such that I c is an atomic formula and 2 c is a s-formula. The s-formula 2 c is said to be the inner s-formula of c l. An input (output) variable is a variable that occurs in the in (out) parameter part of a relational atomic formula, or in the left (right) hand side of a functional atomic formula. 5-formulas are used to combine functional and relational atomic formulas. They define a local environment which is shared by (and allows the interaction among) its components. The s-formula concept allows us to talk about SCA's. Each atomic formula corresponds to an agent, and its variables can be seen as channels connecting different agents. Input and output variables represent the inputs and the outputs of agents. The producer-consumer relationships are modelled by the occurence of the same variable among the output variables of an atomic formula (the producer), and the input variables of a different atomic formula (the consumer). An example of s-formula, and the corresponding SCAt follows. rl(in: dl(V2,V3)i out: ), y2,Y3 ~ x ~ r2(in: d2(v4)i out: vl,v2), r3(in: cl out: v3,v4). 3v u4\ Fig.1 The agents (represented as nodes of the graph) are modelled by the atomic formulasl the producer-consumer relationships (represented by directed arcs) are modelled by the presence of the same variable in the output and input parts of different atomic formulas. Square nodes denote data atomic formulas. The s-formulas defined so far can express a larger class of systems than SCA's, therefore we will introduce some constraints on their form. Let Min(a) (Mout(a)) be the multiset of the input (output) variables of an atomic formula a. Condition 1. eFa-cohr s-formula = S al,a2,...,a n the multiset ..,..,nJ--Ll=i Mout(a i) must be a set. This condition, i.e. the absence of multiple output occurrences of a variable in a s-formula, ensures that every variable is computed by only one atomic formula. In the SCA framework~ this means that for each channel, there is at most one producer. Condition 2. For each atomic formula i a in a s-formula, each variable belonging to i)M in(a must belong to Mout(ak), where k a is an atomic formula occurring in the inner s-formula of a i- This condition forbids to write s-formulas whose input variables do not occur as output variables of any of its inner s-formulas. With this limitation, for any consumer there exists exactly one producer, and the whole SCA results to be a directed acyelic graph. Note that output variables of a s-formula which are not input variables for any formula~ model SCA outputs. 3. REWRITE RULES This Section is concerned with the definition of the rewrite rules which define SCA transformations. A'set of procedures is a set of declarations and rewrite rules. The set of declarations gives sorts to the objects occurring in the rewrite rules. A rewrite rule is a formula of the form l--~r, such that its left part I is a header and its right part r is either empty or has the form of a s-formula, consisting of functional or relational atomic formulas. A header is either: i) a functional header of the form f(tl,...,tm)=t, such that tl,..,tm,t are data terms of sorts Sl,...,Sm,S and feF has sort 1 x s ... x Sm---~ ~s or ii) a relational header of the form r(in: tl,...,tm; out: tm+l,...,tn), such that tl,...,tm, tm+!~...~t n are data terms of sorts Sl,...,Sm,Sm+l,...,Sn and re R has sort I s x ... x Sm---~ sin+ 1 x ... x s n. Rewrite rules allow us to express the dynamics of SCA's. In fact, a rewrite rule allows to rewrite any agent which "matches" its header, leading to the set of agents corresponding to the rule right part. Let f be an atomic formula whose input data terms and output variables are (tl,...,t m) and (Vl,...,v n) respectively. Let e : l -~ r be a rewrite rule, such that f and 1 have the same function (or predicate) symbol, and let (~l,..., mV )' (al'''''an) be the input end the output date terms of the header .1 The atomic formula f can be rewritten by e if there exists an instantiation ,~ of variable symbols to data terms, such that [(~l'"" = ~m)]~ (tl"'" tm)" Note that the variable symbols occuring in the ti's cannot be instantiated, since they represent channels connected to an existing producer. If such an instantiation exists, f can be replaced by a set of atomic formulas, obtained by applying ~ to the rewrite rule right part r (a renaming is performed on the variables that interconnect the atomic formulas of the rewrite rule right part, thus establishing the internal producer-consumer relationships). We are now left with the problem of properly establishing the correspondence between the output channels of f and iriS. This correspondence is defined by the instantiation /~, such that [(v 1 Vn)]/~= [(al, an)l;. ..... .... Note that the occurrence of data constructor symbols in the input and the output data terms of the header ,1 may involve data atomic formulas in the rewriting process~ in both the replaced and the replacing structures. The occurrence of a data constructor symbol in the input of the header corresponds to a selection on the input channel of f. If ~ exists, such a channel is connected to the output of a suitable data atomic formula, which therefore must be included in

Most books are stored in the elastic cloud where traffic is expensive. For this reason, we have a limit on daily download.