J. P. Bowen, `From programs to object code using logic and logic programming', in R. Giegerich and S. L. Graham (eds.), Code Generation -- Concepts, Tools, Techniques, Workshops in Computing, Springer, Berlin, 1992, pp. 173--192.  @ NUS  Home/Search   Document Details and Download   Summary   Related Articles   Check

.... systems at a number of related levels of abstraction from requirements down to hardware [10, 21] The approach has been applied especially in the compilation of high level programs to low level object code, where the compilation of each program construct is based on one or more theorems [3, 34]. A number of extensions such as real time [24] compilation directly into hardware circuits [8, 26] optimization [6, 25] and even decompilation [4] have been explored. Hardware compilation directly into circuits implemented on Field Programmable Gate Arrays (FPGAs) is of increasingly wide ....

Bowen, J.P., From Programs to Object Code using Logic and Logic Programming. In R. Giegerich and S.L. Graham (eds.), Code Generation -- Concepts, Tools, Techniques, Springer-Verlag, Workshops in Computing, pages 173--192, 1992.

No context found.

J. P. Bowen, `From programs to object code using logic and logic programming', in R. Giegerich and S. L. Graham (eds.), Code Generation -- Concepts, Tools, Techniques, Workshops in Computing, Springer, Berlin, 1992, pp. 173--192.

....without necessarily invalidating those that have already been proved correct [26] 7. 2 Rapid prototype compilation It is relatively straightforward to produce a compiler which matchesacompilation scheme such as that presented here very directly using a logic programming language like Prolog [4]. The formal compilation description for each programming construct may be implemented as a Horn Clause. For example, the clauses for SKIP and sequential composition may be implemented as follows in Prolog: cp(skip,S,N1,N2,ROM) N2=N1. cp(P1#P2,S,N1,N2,ROM) cp(P1,S,N1,N1plusN,ROM) ....

J.P.Bowen. From programs to object code using logic and logic programming. In R. Giegerich and S.L. Graham, editors, Code Generation -- Concepts, Tools, Techniques, Proc. International Workshop on Code Generation,Workshops in Computing, pages 173--192. SpringerVerlag, 1992.

....are outputs, and reordering conjoined predicates for efficient execution with this knowledge in mind. Constraints may also be encoded with knowledge of which parameters will be instantiated before use. This allows negation by failure to be used. For a fuller discussion of the issues involved, see [Bow92]. In this case, it is assumed that the source program (q) start address (s) symbol table ( Psi) free locations( Omega and initial register table ( Phi) are instantiated, and the finish address (f ) object code (m) and final register table ( Phi) are to be generated. The example ....

Bowen, J. P.: From Programs to Object Code using Logic and Logic Programming. In [GiG92], pp. 173--192.

....gas burner specifications GB and GBS. When applied to GB it yields the following PL program GBP. GBP = interface copied from GB WHILE( true, SEQ[ GasOff , HeatOn , Set30 , Out30 , Set1 , GasOn , Out1 , Set1 , ALT[ FlOn ALT[ HeatOff SKIP, FlOff SKIP ] Out1 SKIP ] 3. 4 Predicative semantics The link between SL and PL is given byastate trace readiness model for reactive systems [28] presented in a predicativestyle [15] A system is a pair Delta : P consisting of an interface Delta and a predicate P describing all observations that are considered relevant ....

.... and of Burstall and Darlington s approach to transformational programming, but our target is reactive programs, as in [2] To express the intermediate design stages wemix programming and specification notation using a language of mixed terms that contains SL and PL as proper subsets [27,40] A design of a program P from a specification S is then a sequence SjQ 1 j . jQ n jP of (reverse) system implications between mixed terms Q 1 # . # Q n where Q 1 is the given specification S and Q n is the designed program P.Each implication in the sequence is generated by an application ....

[Article contains additional citation context not shown here]

J.P.Bowen, From programs to object code using logic and logic programming, in R. Giegerich and S.L. Graham (eds.), Code Generation -- Concepts, Tools, Techniques, Springer-Verlag, Workshops in Computing, pp. 173--192, 1992.

.... Project Description: ESPRIT Basic Research project 7071 Jonathan Bowen et al. Oxford University Computing Laboratory Programming Research Group 11 Keble Road, OXFORD OX1 3QD Tel: 44 865 273838 Fax: 44 865 273839 Email: procos request comlab.ox.ac.uk Abstract An overview of the current and planned activities of the ESPRIT Basic Research project (no. 7071) on Provably Correct Systems is presented. This is afollow on project to ProCoS (no. 3104) previously announced in ....

.... Project Description: ESPRIT Basic Research project 7071 Jonathan Bowen et al. Oxford University Computing Laboratory Programming Research Group 11 Keble Road, OXFORD OX1 3QD Tel: 44 865 273838 Fax: 44 865 273839 Email: procos request comlab.ox.ac.uk Abstract An overview of the current and planned activities of the ESPRIT Basic Research project (no. 7071) on Provably Correct Systems is presented. This is afollow on project to ProCoS (no. 3104) previously announced in the Bulletin of ....

[Article contains additional citation context not shown here]

J.P.Bowen. From programs to object code using logic and logic programming. In R. Giegerich and S.L. Graham, editors, Code Generation -- Concepts, Tools, Techniques, Workshops in Computing, pages 173--192. Springer-Verlag, 1992.

....with this knowledge in mind. Since Prolog, unlike most highlevel languages, does not evaluate expressions in pa rameters, it is sometimes necessary to recode suchparameters as new variables and add an extra constraint on these variables. For a fuller discussion of the issues involved, see [1]. Here, it is assumed that the source program (p) start address (s) and symbol table ( Psi) are initially instantiated, and the finish address (f ) and object code (m) are to be generated. The example encodings of theorems below use standard pure Prolog. Infix and other operators are defined ....

J.P.Bowen, From programs to object code using logic and logic programming, in R. Giegerich and S.L. Graham (eds.), Proc. CODE'91 International Workshop on Code Generation, Springer-Verlag, Workshops in Computing, 1992. To appear.

....with this knowledge in mind. Since Prolog, unlike most highlevel languages, does not evaluate expressions in pa rameters, it is sometimes necessary to recode such parameters as new variables and add an extra constraint on these variables. For a fuller discussion of the issues involved, see [1]. Here, it is assumed that the source program (p) start address (s) and symbol table ( Psi) are initially instantiated, and the finish address (f ) and object code (m) are to be generated. The example encodings of theorems below use standard pure Prolog. Infix and other operators are defined ....

J.P. Bowen, From programs to object code using logic and logic programming, in R. Giegerich and S.L. Graham (eds.), Proc. CODE'91 International Workshop on Code Generation, Springer-Verlag, Workshops in Computing, 1992. To appear.

....without necessarily invalidating those that have already been proved correct [26] 7. 2 Rapid prototype compilation It is relatively straightforward to produce a compiler which matches a compilation scheme such as that presented here very directly using a logic programming language like Prolog [4]. The formal compilation description for each programming construct may be implemented as a Horn Clause. For example, the clauses for SKIP and sequential composition may be implemented as follows in Prolog: cp(skip,S,N1,N2,ROM) N2=N1. cp(P1;P2,S,N1,N2,ROM) cp(P1,S,N1,N1plusN,ROM) ....

J.P. Bowen. From programs to object code using logic and logic programming. In R. Giegerich and S.L. Graham, editors, Code Generation -- Concepts, Tools, Techniques, Proc. International Workshop on Code Generation, Workshops in Computing, pages 173--192. SpringerVerlag, 1992.

....Germany Email: mf informatik.uni kiel.dbp.de Ernst Rudiger Olderog FB Informatik, Universitat Oldenburg Postfach 2503, 2900 Oldenburg, Germany Email: Ernst.Ruediger.Olderog arbi.informatik.uni oldenburg.de Anders P. Ravn Department of Computer Science Technical University of Denmark, bldg. 344 DK 2800 Lyngby, Denmark Email: apr id.dth.dk Abstract The goal of the Provably Correct Systems project (ProCoS) is to develop a mathematical basis for development of embedded, real time, computer systems. This survey paper introduces novel specification languages and verification techniques for ....

....Germany Email: mf informatik.uni kiel.dbp.de Ernst Rudiger Olderog FB Informatik, Universitat Oldenburg Postfach 2503, 2900 Oldenburg, Germany Email: Ernst.Ruediger.Olderog arbi.informatik.uni oldenburg.de Anders P. Ravn Department of Computer Science Technical University of Denmark, bldg. 344 DK 2800 Lyngby, Denmark Email: apr id.dth.dk Abstract The goal of the Provably Correct Systems project (ProCoS) is to develop a mathematical basis for development of embedded, real time, computer systems. This survey paper introduces novel specification languages and verification techniques for ....

[Article contains additional citation context not shown here]

J.P. Bowen, From programs to object code using logic and logic programming, in R. Giegerich and S.L. Graham (eds.), Code Generation -- Concepts, Tools, Techniques, Springer-Verlag, Workshops in Computing, pp. 173--192, 1992.

....space. However they are presented in the report on which this paper is based [11] for those who are interested in the full language. 4 Rapid Prototype Compiler The compiling theorems shown here may easily be transformed into Horn clauses. Thus it is feasible to prototype them as a logic program [1]. However, to produce an executable compiler, it is necessary to constructively generate each of the constructs of the language. This is relatively easy for the sequential aspects of the language. Theorems 1 to 3 may be transliterated very directly into a language such as Prolog [7] Clause 1: ....

J.P. Bowen, From programs to object code using logic and logic programming, in R. Giegerich and S.L. Graham (eds.), Code Generation -- Concepts, Tools, Techniques, Springer-Verlag, Workshops in Computer Science, pp. 173--192, 1992.

....are outputs, and reordering conjoined predicates for efficient execution with this knowledge in mind. Constraints may also be encoded with knowledge of which parameters will be instantiated before use. This allows negation by failure to be used. For a fuller discussion of the issues involved, see [Bow92]. In this case, it is assumed that the source program (q) start address (s) symbol table ( Psi) free locations ( Omega Gamma and initial register table ( Phi) are instantiated, and the finish address (f ) object code (m) and final register table ( Phi) are to be generated. The example ....

Bowen, J. P.: From Programs to Object Code using Logic and Logic Programming. In [GiG92], pp. 173--192.

....themselves as convenient links between theory and practice for the techniques we will describe; logic programming, and functional programming. Logic programming has already been found to be convenient for the direct expression of the semantics of source program constructs in terms of object code [4]. Such specifications logic relationships can be proved correct using purely mathematical techniques when they are read as theorems [22] but read as programs, they are compilers. The technique has been applied to a subset of occam for the transputer, demonstrating that it is applicable to ....

J.P. Bowen, From programs to object code using logic and logic programming, in R. Giegerich and S.L. Graham (eds.), Code Generation -- Concepts, Tools, Techniques, Springer-Verlag, Workshops in Computing, pp. 173--192, 1992.

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.