--- title: "Automatic Programming Using Abstract Data Types" authors: - "Gérard D. Guiho" doi: "" url: "https://ijcai.org/proceedings/1983/1" pdf: "https://ijcai.org/proceedings/1983/0001.pdf" venue: "Proceedings of the Eighth International Joint Conference on Artificial Intelligence" year: 1983 pages: "1-8" track: "Automatic Programming" keywords: --- # Automatic Programming Using Abstract Data Types Gérard D. Guiho *Proceedings of the Eighth International Joint Conference on Artificial Intelligence*, pages 1-8. ## Abstract In this paper we first try to characterize one meaning of automatic programming. We consider it to be one part of the Progranming environment related to Artificial Intelligence techniques. We then illustrate an automatic progranming process, on a simple example, using an Abstract Data Type theory to .hl.ch ~add the rot ion aE schemes which are particularly useful in program derivation from Abstract Type decomposition. We conclude that all the concepts treated in this paper must be contained in one way or another in any automatic prcbramming system. However this necessitates further study in such theoretical fields as Abstract Data Type Theory, Specification languages, Theorem provers or proof cheekers and rule rewriting systems. ## Full text ## AUTOMATIC PROGRAMMING llSING ABSTRACT DATA TYPES ## Gerard Guiho Universite Paris Sud LRI - Bat. 490 91405 ORSAY - FRANCE ## ABSTRACT In this paper we first try to characterize one meaning of automatic programming. We consider it to be one part of the Progranming environment related to Artificial Intelligence techniques. We then illustrate an automatic progranming process, on a simple example, using an Abstract Data Type theory to .hl.ch ~add the rot ion aE schemes which are particularly useful in program derivation from Ab­ stract Type decomposition. We conclude that all the concepts treated in this paper must be contai­ ned in one way or another in any automatic prcbram­ ming system. However this necessitates further study in such theoretical fields as Abstract Data Type Theory, Specification languages, Theorem pro­ vers or proof cheekers and rule rewriting systems. ## I GENERALITIES I. I. In my opinion the concepts implied in the words "Automatic Progranming" are not very precise and may even seem completly unrealistic. However many people, like myself may consider that even if they seem vague and sometimes unrealistic they ap­ pear worthwhile for studying. In the first part of my papei, I will try to specify the definition of these concepts, created by the juxtaposition of the two words "Automatic" and "Programming". In Webster's dictionary, we can see that "au­ tomatic" can be the obtention of something which can be produced without thinking, by habit or re­ flex. In this case, Automatic Progranming could be considered as a kind of programming methodology, which is sufficient to follow to obtain a good program. This can only be applied in areas where the prograrrming process is repetitive enough that a method can grasp the mechanical aspect. In this way .. \_in the business-oriented programming field, some program generators or methodologies can be considered as automatic programming. A second meaning to the word automatic con­ cerns one action which is done by itself. We coilld then look for a programming technique which is en­ tirely produced by any kind of mechanism. This is ~ Artificial Intelligence approach. In this sense we could consider building a system which would receive the specification of a problem as input and which will give a program as output. This field is often called Program Synthesis. The input specification can be formal specifications (as logic) [I) [ 2) , Examples [ 3) [ 4) [ 5) or Natural Language. Taking into account the research which has been done on this subject during the last five years and my own personal experience, I think that this approach is only possible for restricted fields of application and toy problems. In other cases the specification language is close to a programming language and it is more a compiling technique than automatic programming. I am there­ fore convinced that this approach can be useful locally but that programmingj in the general sens~ will never be completly automatic. A third sense to the word automatic will also help us. It characterizes one action which is done using automatic equipment. This dictionary defini­ tion is in fact recursive !! That leaves us now to consider that it is not the action of programming which has to be automatic but the equipment which could help do this action. Lastly we can interpret "Automatic Programming" as the programming action using a computer, which allows us to write pro­ grams in the best way possible". That does not im­ ply that the whole programming process has to be automatic. Unfortunately,this definition is too general. If any sys tern used during the programming process is relevant to automatic programming then most of the programmers are in fact using automatic pro­ gramming techniques without knowing it. Is a text editor, a compiler, a linker, ... relevant to au­ tomatic programming ? And is there any difference between "Automatic Programming" and "Programming Environment" ? In fact I consider that automatic programming is a part of what is called programming enviroment. It consists of the tools which are the most advan­ ced in the programming environment and which are directly related to the programmer. We are very close here to an Artificial Intelligence paradigm because the action of programming can be conside­ red as one of the most difficult and intelligent action a human can do. Sofisticated tools which could help the programmer during this powerful ac­ tion may be relevant to the Artificial Intelligen­ ce field. However, even if the line between Artificial Intelligence and classical Computer Science is not really precise in Automatic Programming, I consi­ der that it is a domain in which many different Artificial Intelligence techniques can be extreme­ ly useful. This must be a challenge for Artificial Intelligence people. It is not a coincidence if the first and most powerful programming environments came from the Artificial Intelligence community. (Interlisp, Maclisp ... ) I.Z. I will summarize some fields of Artificial In­ telligence and just give some areas where they could be profitable in automatic programming. - Natural Language Understanding--This sub­ field could be very useful, not in the command to be given to a system but to help the programmer in the various commands and utilities of the program­ ming environment. For an experienced programmer, the the commands he knows have to be very short. They are generally keys. The problem is that when we want to explore some new possibilities, we do not know precisely the keys or the successions of keys to use for these new possibilities. Looking through the documentation (even in line) is some­ times boring. The "a propos" command under emacs is useful but is only a key word search. The develop­ ment of a natural language interface would allow a sophisticated help system which would then be very effective . - Expert Systems--I do not think an expert system can be constructed at the present in the program-creating process because it is too diffi­ cult and may even be outside of classical expert systems approach. However, in many parts of the programming process an expert system viewed as an assistant can be used. These systems have to be se­ parate tools : - . The organisation of large programs. How to find some information in a large base of programs or data types ? What has been done until now and what would be the most suitable to do now etc ... ? It is a knowledge-based oriented sys tern [ 6] . - . The process of transforming programs [7) . - . Restricted areas. When the field is very small and the derivation of the program from the specification very easy, it would be fruitful to design some small expert systems. - . The validation of programs using test sets. The generation of the test set for programs is ne­ ver completly satisfactory and is a difficult art. Testing a program can be relevant to Expert System techniques. - Theorem Proving--Testing programs are not sufficient and in the future most of the programs will have to be proven, at least partially. Many interactive systems will have to be designed in or­ der to help the programmer prove the correctness of this work. This domain is highly related to Theore­ tical Computer Science because most of the concepts in languages or programs have not yet been suffi­ ciently studied to be used in practive for real programs. Some systems as GYPSY [8), STP [9), FORMEL [ 10] are milestones towards this approach. The rest of this paper will try to show that even for small examples, the proof can be long and the material involved very sophisticated. - Other techniques--Many other aspects which only use heuristics can be very useful in the pro- gr&ming process . I will just give some of them here but this is not exhaustive. -Help during the programming process--Proposing program schemes, data decomposition, programs which are "close" to the one the programmer is actually doing etc ... - Intelligent display of all the information needed during the programming process (a,screen with a multiple-window oriented editor). - Organisation for work scheduling. ## II PROGRAM CONSTRUCTION We will .now describe one proposal for a program construction technique. It is not aimed to be enti­ rely general but shows many concepts which, in one form or another, are necessary in every futu~e auttr matic programming system. It is now beginning to be admitted that a li­ brary which is useful in the programming p!·ocess must contain both data and programs. All these ob­ jects have to be encapsulated in modules. Some of these modules involve descriptions of powerful data types with basic operators ; some others involve sets of programs with one common functionality. All these modules contains two parts. One wch shows that which is visible outside of the module, which attempts to describe the specification of the manner in which to use it. The second part des­ cribes how effectively the elements of the modules are implemented. This is one of the most important aspects of ADA with the PACKAGE and PACKAGE BODY parts. Generally the description part (which we will call the specification part) only contains the pro­ file of the operations which are visible outside the module and few other helpful things for type chee­ king and documentation. However, even if this aspett constitutes a major improvement, it does not allows us to produce proofs. The nature of the objects which have to be grasped in our system can be represented as : ![Image](https://ijcai.org/proceedings/1983/fulltext/1/image_000000_5769e8505843c2a39c5d143db135d4cfbfadcd725a849ee2eadcdc96585a025f.png) where ## I. Data Type Specification (DS) We use Algebraic Abstract Data Types in an ex­ tended manner which will be described in sectioniTI. According to the theory, an Algebraic Abstract Dam Type specification denotes a class of Algebra Alg and i~ our theory this dasshas one initial algebr~ T~ . (1e for each algebra A in Alg there exists one u~ique morphism h : TL~A. L ## 2. Data Implementation (DI) Generally the Data Implementation is not v~ : sible to the user (and it must not be visible). We will consider that the Data Implementation repre­ sents nne of the algebra in Alg denoted by the ab­ stract type specification. The fact that there e­ xists one morphism between T (which is a particu­ l~r Algebra of Terms) and A ~elps us prove proper­ t1es or theorems on the type using T . These pro-. '11 · E pert1es w1 be propert1es of any implementation. Of course the correctness of the implementation h~ to be pro':'en in the same ways that many proper­ t1es concern1ng abstract specification. That is done once for all and could be considered as the responsability of the data type designer. Note that our class of algebra is the class of finitely ge­ nerated algebras so that we can use term rewriting and structural induction for producing proof. ## 3. Procedure specification (PS) In a first approximation we will consider ~e­ cifications in an algebraic manner. This will be easier for proofs but it may lead to specifications which are not really readable. I consider that there does not exist for the moment an effective convenient specification language. If one such ' language would exist, its semantic would have to be expressed algebraically, but for our purposes here I have chosen to express it directly in its algebraic form. ## 4. Procedure implementation (PI) First we need a programming language with a well-defined semantic in order to produce proofs. Section IV will describe such a toy language. �iv~n a.program P written in such a language and prov1ng 1ts correctness may not be sufficient. These properties are proven in fact in an exten­ sion of TL, the initial term algebr~ : TL + p and the program will actually be used in an algebra A + P. The fact that there exists an homomorphism h : T~~A does not prove that it can be naturally ex~enaed to an homomorphism n : TE + P ~A + P. Th1s has to be proven again and it can be done either - -By proving it on each program!! - B~ res~ricting the form of programs or by d1rect1ng the program construction such that any morphism can be extended. - By using monomorphic abstract types. ## 5. Program construction Two main methods can be used in building pro­ cedures concerning a problem we have in mind or which is expressed in a natural language manner : - . a .. Knowing a family of Data Types Specifica­ t1?n~ bu1ld a procedure specification using any in­ tu1t1ve method and then derive a program. ![Image](https://ijcai.org/proceedings/1983/fulltext/1/image_000001_7e71b6cf1690a056a3a69325dcb34ab1fdaaaa72cc47c02691f4794192dec0ea.png) The problem whith this method is that even for short specifications, the risk of error is high (it may be even higher than direc tly deriving the program if the specification language is obscure). Subsequently the program will be wrong and if the procedure specification represents in some sense a "cont:act", this could be dangerous. One other pro­ blem 1s that only when the program is effectively tested that some errors will occur. It might not be easy to see where they correspond to a mistake in the specification. The risk is that the programmer will directly change the program!! One could say that we have some executable specifications but the other risk is that the program might easily follow the specification and could be highly uneffective. - b. Knowing a family of Data Type Specifica­ tions, build a procedure specification, then build a program separately and prove the correctness of the program versus the specifications. Proof ![Image](https://ijcai.org/proceedings/1983/fulltext/1/image_000002_7352e4af01e546a75be0dad34046e7c93e0bdb8d481092a1f51d976d7dc6c532.png) Here we have more chance to make errors in the two constructions but the errors will not be neces­ sarily the same. The proof mechanism will help us to correct. the two parts. In my experience I always made aprox1mately the same number of mistakes in writing programs or specifications. Trying to prove the correctness always leads me to reconsider both. The risk is that if the specification is too far from the implementation (highly non executable spe­ cification for instance) the proof could be very difficult. One other way would be to extract automatical­ ly the test set from the specification in order to test the program. [II]. This is the type of program construction technique we wil use in further sections with a syste­ matic methodology for building programs. It could help us reduce the amount of errors when we try to express our intuition.Wewill use one toy example all along (the gcd problem) because it is sufficiently complex, the concepts significant and sufficently short to be shown in one paper. ## III ALGEBRAIC ABSTRACT DATA TYPES We will use the now classical theory of abs­ tract types which is directly inspired from ADJ [ 12), Goguen [ 13] [ 14], Broy & Wirsing [ 15], C'Jmplemented by work from Bidoit [ 16], Kaplan [ 17], myself, Boisson and Pavot [ 18]. Our addenda concern principally the presentation of type, the use of positive conditional axioms and the error mechanism. The schemes are direct extensions of the de­ composition schemes of C. Gresse [ 19] (same procee­ dings). An abstract type is given by - I. A signature represented by a setS of S~rts and a set L of symbols with an arity ing/(s) . 1his differs fr~m the usual theory where the arity be­ longs to S ). We use, as Goguen does, overloading and coercion extensively. The notation of operators is similar to OBJ [ 12] . ## 2. A set of positive conditional axioms. These axioms (as in Goguen [ 14]~ontains the sort in which the equation has to be considered. The operators are multioperators and can have more than one output . In fact, their interpretation is a function from the domaines of their input to the union of domaines of their output (which have to be disjointed). The operators have to be total on the ground terms but can be partial on terms with va­ riables. Using some kinds of presentation and with some properties, it can be shown that there can exist one initial algebra of terms in the class of specified algebras . More details are available in Boisson & All [ 18] . ## 3. Some induc tion schemes These induction schemes will be useful during the construction and the proof process. They will be described more precisely in the appropriate sec­ tion. They correspond in a sense to the induction schemata in Affirm [20]. ## 4. Some theorems This part contains properties or theorems which can be deduced from the axioms. These theo­ rems may be useful in the proofs. Fig. I describes the specification of the po­ sitive integers t ype . We assume that the type Bool which represents the booleans is known somewhere else with all it's suitable operations and axioms. We can make the following remarks on thi s example : - We define here three sorts. The zero sort is - very convenient for constructing programs and for specifying this type. - The notation int = int+, zero is just synta~ tic. It is to avoid writing int+, zero everywhere in the type. - The underscore ( ) shows the places of the operands with the disfix-notation of operators. - There are plenty of overloadings in this sp~ ­ cification. For instance there are four + operato~! - When there is more than one sort in the left part is ~ int of the arity of one operator, it means that it multioperator. For instance P has two outputs: and zero . - There exists also multiaxioms (a syntactic level) in the way that an axiom is repeated when there is some ambiguity in the type of operators or when there are more than one sort before the axiom. For instance ``` int : X + 0 = X or bool: x < 0 False means zer~ int bool bool X + 0 X X + 0 = X x zer~ < 0 x int < 0 False False ``` See figure I next page for pvesentation of the type. - There are conditional axioms like x egal y ~ x div y = True In fact a correct definition would be : x egal y = True ~x div y = True We accepted this syntactic simplification, in order not to overload the axioms but they are all positive conditional. - We can see with some examples how the initial term algebra is. - 0 is in sort zero - sO is in sort int+ and {snOifor n ~ I} arein:int+ because s is not a multioperator. These terms can be considere~ as representative of classes of terms in int - psO is in zero because of the first axiom - ppsO does not exist because p does not apply to sort zero - sO - ssO 0 - sO by axiom 3 erint by axiom 4 Then it is in inter - The term sO + (sO - sssO) does not exist It can be proven that there is no ambiguity for any ground t erm and then this term algebra is ini­ tial. - The axiom inter : x = erint collects all the error terms into one single class without avoiding all the classical problems with the errors in abs­ tract data type. - It is necessary for the evaluator to do type cheeking during the evaluation process in order~ choose the correct ax~oms or to detect terms which do not exist . In fact these terms will not be gene­ rated with correct programs. It might be possible here to add some operators which could be applied to inter to get error propagation and these t erms would then exist (for instance : + : (int, inter) (int, inter) + int, inter - in spite of the existing one !) - An equation can be used iff its two sides exist and have the same type. Then, for instance, the third theorem int : x + (y - x) = y means If y - x € int then the two sides of the equation can be substituted and this condition has to be kept during the evaluation of terms. ``` + ``` ## I. Syntax Our programming language here is very simple . (but powerful), which is in one sense an algorith­ mic specification language but it is suitable for our purpose. ## Type Int , zer~, inter Int = Int , zero Si!!;nature 0 -+ zero int -+ int + S-. + + P- ~nt -+ in~ , zero int -+ int , zero, inter + int int -+ int egal int int -+ bool - < int int -+ bool - - int int bool > -+ - . +. + diy\_ ~nt ~nt -+ bool - psx = x X - 0 = X Axioms int int int, inter inter SX - sy X - y 0 - sx = erint X + 0 = X x + sy = s(x + y) in~ int bool bool bool x egal y ~ x divY = True x < y~xdivy xdiv(y x) x > y ~ x div y = False inter bool bool bool bool bool bool bool bool bool bool Schemes x = erint x egal x = True 0 egal sx = False sx egal 0 = False sx egal sy = x egal y x < 0 = Fal,;e 0 < sx = True sx < ~y = h < y 0 > x = False sx > 0 = True sx > sy = x > y SHI :: (x:int+ ; 0 -+ out SH2 :: SHII [ x: int +, y : int + ~ z = x-y : int +, y] erint -+ SHI2 SHI2 Theorems 0 -+ out [x:int+, y: int+ ~x, z erint -+ SHII 0 -+ out int X - y 0 ~X egal y True int .. X + y y + X int X +(y x) = y bool X div y " X div z = x div(y y - X ~ X y ~ y - X 0 + z) " x div y Figure ## IV PROGRAMMING LANGUAGE Figure 2 (next page) shows the syntax of this lan­ guage . ## 2 . Semantic The semantic is given here as a rewrite sy&E~. This is particularly useful if we want to evaluate procedures on terms in order to make proofs ! We will use some auxiliary fonctions or combinators in order to shorten the description . is the basic construction of the semantic. Think of it as the meaning of one element of program (which has to be considered as abstract syntax even if it is very close to the concrete syntax) in some environments and with some particular continuacioas. It returns return with one environment or an excep­ tion or kil-1-.---- One environment can be considered as a list of couples [<x., v.>] where x. is a variable and v. its value ifr so~e algebre l. Env(x) = v. means Ehe value of x in the environment Env. It ig equal to v. if it exists <x., v. > otherwise it is undefined. W~ will assume all~the~functions to be strict but we will not use this assumption because of the pro­ gramming construction process. ``` le . name means the instruction list of "le" associated to name F. outputvar means the output variables of procedure F F. inputvar means the input variables of procedure F F. body means the body of F ``` Except ? <dP<value)) =True if in the algebra on which the procedure is ap­ plied , ~p(value) will give a domain which is not of the output sort. The following rewrite rules give the meaning of a succession of instructions. [ l. I 1 ] means a continuation by a list of instrucEionse(l.) and a list of exception names with a list of instrfictions related tooochnane(le).Jhese two rules show the semantic of raise. .).(.(raise name, Env, [l.ll].c)-+ This rule is the semantic of one basic opera­ tion which has to apply directly into an algebra Figure 2 ![Image](https://ijcai.org/proceedings/1983/fulltext/1/image_000003_b1f14ad2af9671979dbcf3d496dd2e948ee15069d50469d929c804eab7a3a1eb.png) These three rules are for the semantic of the cal­ ling of oth~procedures. It uses one auxiliary function ~ ..]'. Ji<z: = F(v), Env, c) +J(.(z ~~<}£.(~,[<F. inputvar, Env(v)>], [F.corpsJ0]), F), Env, c) ![Image](https://ijcai.org/proceedings/1983/fulltext/1/image_000004_49dabb286abc2265d7775b7cdd4462fc5bead073f49d024a390924b959c0b0a9.png) All the rules which follow show the semantic of the bloc construction . It shows taht the begin end construct is a kind of parallel evaluation of processes. Here are the successions of processes. When a process is killed, it leaves the others to work normally. If a process terminates normally it tries to export its results after killing the others. If a process raises one exception and if this exception belongs to the without part of the begin end it is like a killing of the process, else it ~like a normal terminating one. These three rules give the final result of the begin end construct following the process which succeeded. ![Image](https://ijcai.org/proceedings/1983/fulltext/1/image_000005_c6e9b3296f833bf5076fb8645b7c994b7fc98b93ec1a7a371d2d524d9abc5fed.png) This langage is in fact too rich and we can prove that the extension of homomorphism h (bet­ ween TE and any algebra of Algl.) cannot be done for every program. We will restrict our programs such that the definition of programs plus the defi­ nition of the semantic plus the definition of abs­ tract types is a canonical system. This means ter­ minating programs and no real nondeterminism. The schemes which belong to the astract types will help us in doing that. Not that this eliminates programs such that Proc y + Anynumber (x: int) begin y : = x 0 y : = Anynumber (s(x)) end endproc which is unbounded determinism. In order to help the proof process we will also suppose that we have unique assignment pro­ grams (we can then replace the : = by equalities during the proofs). The responsability to obey all these restrictions is left to the programmer be­ cause it is highly non-decidable for all programs. ## V PROGRAM CONSTRUCTION PROCESS One program at the begining can be considered as a name, a set of input variables and their type~ an output variable and its type and a list of excep­ tions which can be raised by the program. Let y:t'+F(x:t)raise ex! ; such an expression where to simplify we use-Qnly one input variable and one exception name. The program construction process consists of choosing a set of input variables and to use one of the schemes which belong to the description of the corresponding types. This transformation can be expressed as in figure 3 where : - x, x', j ... are only one variable but this scheme can be generalized to more than one as in the example. . - . The inex: mean the exceptions or the sorts which can be obtained using multioperators@p. or ~p' . such that the subscheme SH: can be evalGated normllly. J - . The oute~ mean the exceptions or the sorts such that no subscheme SH: can be used without gi­ ving a sort outside the ndrmal output of the opera­ tors. - We assume that for each scheme SH on x there exists one function V : T -+IN such that : - Vx E T V(x') < v(x) on each subscheme SHii. That means that the scheme corresponds to a well-defined or dering on x and is particullarly useful for making proofs. - In the program generated - ~SP .... denotes subproblems which have t0 be ex­ press~d directly by the user or as new subproblems to be solved in the same way. - erF is one exception which is systematically ad­ ded to each procedure. It can be simplified if it can be proven at the end that it is useless. - We assume here that we can use recursion on F(t : = F(x')) but this can be easily avoided. If the recursion is used then an erF exception with its corresponding subproblem ~SPerF is generated. -An exception for each subproblem ~SPi(ie er ~SPi) and a new subproblem are generated. - All this is immediately and automatically genera­ ted simply by pointing to a scheme. If some of the subproblems seem to remain unsolved or not easily expressed, the programmer can choose another scheme and so on ... - Example We will construct the well known gcd program which can be considered as a toy problem, but which is more difficult that most of the practical real problem~ i~ the conc~pt~ it.in~0kes. The heading is: Proc p:1nt + gcd(x:1nt ,y:1nt ) We will choose to use the scheme SH2 on type int+ This leads automaticallv to : Proc p:int 1 + gcd(x:int~,y:int+)raise ergcd ; -- begin without erint ; --- z gcd(z,y) 0 z : = y-x ; P 1 : gcd(x,z) ## Except when 0 $SP 3 er~SP I : ~SP S eq;(cd : ~SP 4 er~SP 2 : ~SP 6 end endproc x-y P 1 We have to "manually" build the subproblems ~Pi. It is easy to guess that ~SP 1 ~s P:P 1 ~SP 2 1s P:Pl which cancel er~SP 1 and er~SP 2 then ~SP 5 and ~SP 6 · ~SP 3 is P:=x ~SP 4 by raise ergcd An easy transformation leads then to thefinal program: Proc p:int++gcd(x:int+, y:int+) ~gin without erint; ----z:=x-y; p:gcd(z,y) D z:=y-x; p:=gcd(x,z) except when O:p:-x end en(fjiroc which is quite elegant and well-structured. Proc y + F(x: T) raisP. narne, ... ,erF ## except when ; outexk ~SPE~ erF name ~SPerF ~ name end en<fi}roc idem. Idem ## VI PROOF As there is nothing really special in the proof process, we will only describe it on the example in order to conclude. We will assume for instance a "non executable' algebraic specification of gcd is given by - I. Let us prove a first lerna We will use the induction following the s~rne. - a) First subscherne - b) Second subscherne - c) Exception D 2. Let us now prove the first part of the speci­ fication gcd(x, g) div x A gcd(x,y) div y Will use the induction on the scheme in the same way : ## a) First subscherne gcd(x, y) = gcd(x - y, y) = gcd(y, x - y)by lemma I - gcd(y, x - y) div y A gcd(y, x - y) div x - y by induction - gcd(y, x - y) div y + (x - y) A gcd(y, x - y)di.v y by theorem of int+ - gcd(x, y) div x A gcd(x,y) div y by subscherne I and theorem 3 of int+. - b) Second subscherne - c) Exception gcd(x, y) = x then x - y = 0 and x = y gcd(x, y) div x A gcd(x, y) div y = s div x A y div y which is true by property ofdiv. 3. The second part of the specification is now to prove z div x A z div y =>D (gcd(x, y) < z) which can be proven using the same kind of in­ duction. This example shows that the proof is not very easy, even for such a simple example because of the theorems or lemmas which have to be used. In our opi­ nion, this kind of proof cannot be done automati­ cally by a present theorem prover (with the disco­ very of lemmas).A nice proof checher would be pre­ ferable. ## V CONCLUSION This method, this toy example and the sim­ ple proof do not intend to describe all the tools which have. to be in such a system. \le claim here that when we try to be very precise (and we have to when we build correct programs) all the concepts which belong to this paper have to be contained in one way or another in the system, which leads to many difficult theoretical problems not completely solved at this time. What we can hope for in the near future is the ef­ fective implementation of such partial systems which will become more and more powerful, coupled with meaningful research on abstract data type the­ ory, Specification lan~uages, Theorem provers or proof cheekers and rule rewriting systems . ## "ACKNOWLEDGMENTS." The authors wishes to thank M. Bidoit, M.C. M. C. Gaudel, C. Gresse, S. Kaplan for many exci­ ting discussions on this subject. ## References 1. I I Manna, Z. & R. Waldinger, "Deductive synthesis of the unification Algorithm" In Computer Pro- gram synthesis methodologies. A. Biermann & G. Guiho Editors. D. Reidel Publishing Co 1983. 2. Bidoit, M.& C. Gresse & G. Guiho, "A system which synthesiezs array manipulating programs from specifications. Proc 6th IJCAI-79. Tokyo pp. 63-65. . 3. I Kodratoff, Y, "A class of functions synthesized from a finite number of examples and a LISP pro- gram shceme". International J. of Comp. and Inf. Sciences 8, 1979, pp. 489-521. 4. Jouannaud,J. P . & G. Guiho, "SISP/I An inter- antive system able to synthesize functions form examples" . Proc 5th IJCAI. 5. M.I.T., August, 1977. 6. Biermann, A. W. & D. R. Smith, "The hierarchi- cal synthesis of LISP scanning programs". In- ~rmation processing 77, North Holland, 19~ pp. 41-45. 7. M6riconi, M. "A designer/verifier's Assistant" IEEE Transactions on Software Engineering, Vol Se-5 N 6 4, July, 1979. _ 8. Barstow, D. R. "Automatic Construction of Al- gorithm and Data Structures using a Knowledge base of Programming Rules". PHD Dissertation, Stanford Memo AIM-308, 1977. 9. G. Guiho 9 10. Good D. & All, "Report on the language Gypsy" Version 2. 0. Institute for computing Science and computer applications. The University of Texas. Austin Texas 1978 . 11. Shostak, R. E. and R. Schwartz, Melliard-Smith P . M. STP : 'A Mechanized Logic for specifica- tion and verification". 6th conference on Au- tomated Deduction, NY 1982 . 12. Huet, G. "Projet Formel", INRIA, France 1983. 13. Bouge, L. "Modelisation de la notion de test et de programmes". These 3e cycle LITP Paris Novembre 1982 14. Thatcher, J. W. and E. G. Wagner and J. B. Wright, "Specification of Abstract Types using conditional axioms , IBM report 6214, Septem- ber 1976. 15. Goguen, J. A. and J . W. Thatcher and E. G. Wagner, "An Initial Algebra approach to the specification, correctness and Implementation of abstract data type. IBM report KC 6487, October, 1976. 16. Goguen, J. "Order Sorted Algebras : Exceptions and Error Sorts, coercion and Overloaded opera- tors. Report II 14, S.R.I. December, 1978. 17. IS) 18. Wirsing, M. and M. Broy, "Abstract data types as lattices of finitely generated Models". 9th MFCS ,Rydjyna, September, 1980. 19. Bidoit, M; "Algebraic Data Types. Structured Specifications and Fair Presentations". Collo- que AFCET/MA,Paris, March, 1982. ----- 20. Kaplan, S. "Un langage de specification de ty- pes abstraits algebriques". These 3e cycle LRI-Orsay, Fevrier, 1983. 21. Boisson, F. and G. Guiho and D. Pavot, "Alge- bres a Operateurs Multitypes" . Rapport interne LRI-Orsay, Mai, 1983. 22. Gresse, C. "Automatic programming from Data Type decomposition paterns". 8th IJCAI-83, Karl- sruhe, August, 1983. 23. Loeckx, J. "Proving Properties of algorithmic Specifications of Abstract data Types in AFFIRM" . Memo-29-JL U.S.C July 1980.