User:Tyugu/sandbox
Structural synthesis of programs (SSP) is a special form of (automatic) program synthesis that is based on propositional calculus. More precisely, it uses intuitionistic logic for describing structure of a program in such a detail that the program can be automatically composed from pieces like subroutines or even computer commands. It is assumed that these pieces have been implemented correctly, hence no correctness verification of these pieces is needed. SSP is well suited for automatic composition of services[1] for service-oriented architectures and for synthesis of large simulation programs [2] [3].
History
Pioneering works in automatic program synthesis belonged to the artificial intelligence field and were aimed at automatic problem solving. The first program synthesizer was developed by Cordell Green in 1969.[4]. Approximately at the same time, a number of mathematicians (R. Constable, Z. Manna, R. Waldinger) explained possibilities of the usage of logic for automatic program synthesis. Practically applicable program synthesizers appeared considerably later.
Idea of the structural synthesis of programs was introduced at a conference on algorithms in modern mathematics and computer science [5] organized by Andrey Ershov and Donald Knuth in 1979. The idea originated from G. Pólya’s well-known book on problem solving [6]. The method for devising a plan for solving a problem in SSP was presented as a formal system. The inference rules of the system were restructured and justified in logic by G. Mints and E. Tyugu [7] in 1982. A programming tool PRIZ [8] that uses SSP was developed in eighties. The most recent IDE that supports SSP is CoCoViLa [9]- a model-based software development platform for implementing domain specific languages and development of large Java programs.
About logic of SSP
SSP is a method for composing programs from already implemented components (e.g. from computer commands, methods of objets etc.) that can be considered as functions. A specification for synthesis is given in intuitionistic propositional logic by writing axioms about the applicability of functions. An axiom about applicability of a function f is a logical implication
X1 ∧ X2 ∧ ... ∧ Xm → Y1 ∧ Y2 ... Yn,
where X1, X2, ... Xm are preconditions and Y1, Y2, ... Yn are postconditions of application of the function f. In the intuitionistic logic, the function f is called realization of this formula. A precondition can be a proposition stating that input data exist, e.g. Xi may have the meaning “variable xi has been computed”, but it may denote also some other condition, e.g. that there are resources for using the function f etc. A precondition may be also an implication of the same form as the axiom given above, then it is called a subtask. A subtask denotes a function that must be available as an input when the function f is applied. This function itself must be synthesized in the process of SSP. In this case, realization of the axiom is a higher order function, i.e. a function that uses another function as an input. For instance, the formula
(state → nextstate) ∧ initialState → result
can specify a higher order function with two inputs and an output result. The first input is a function that has to be synthesized for computing nextState from state, and the second input is initialState. Higher order functions give generality to the SSP -- any control structure needed in a synthesized program can be preprogrammed and used then automatically with a respective specification. In particular, the last axiom presented here is a specification of a complex program -- a simulation engine for simulating dynamic systems on models where nextstate can be computed from state of the system.
References
- ^ Maigre, Riina; Küngas, Peep; Matskin, Mihhail; Tyugu, Enn (2009). Dynamic service synthesis on a large service models of a federated governmental information system. International Journal on Advances in Intelligent Systems, 2(1), 181 - 191.
- ^ Kotkas, Vahur; Ojamaa, Andres; Grigorenko, Pavel; Maigre, Riina; Harf, Mait; Tyugu, Enn (2011). CoCoViLa as a multifunctional simulation platform. In: SIMUTOOLS 2011 - 4th International ICST Conference on Simulation Tools and Techniques : March 21-25 - Barcelona, Spain: Brussels: ICST, 2011, [1 - 8].
- ^ Grosschmidt, Gunnar; Harf, Mait (2009). COCO-SIM - object-oriented multi-pole modelling and simulation environment for fluid power systems. Part 1: Fundamentals. International Journal of Fluid Power, 10(2), 91 - 100.
- ^ Green, Cordell (1969) Application of Theorem Proving to Problem Solving. Proceedings of the International Joint Conference on Artificial Intelligence. Donald E. Walker and Lewis M. Norton, editors, Gordon and Breach Science Publishers, New York, New York, 219–239.
- ^ Tyugu, E.H. (1981). The structural synthesis of programs. In: Algorithms in Modern Mathematics and Computer Science : Proceedings, Urgench, Uzbek SSR September 16-22, 1979: Ershov, A.P.; Knuth, D.E. (Eds.) Berlin: Springer, 1981 (Lecture Notes in Computer Science; 122), 290 - 303.
- ^ Pólya, G. (1957) How to solve it. Princeton University Press.
- ^ Mints, G.; Tyugu, E. (1982). Justification of the structural synthesis of programs. Science of Computer Programming, 2(3), 215 - 240.
- ^ Mints, G.; Tyugu, E. (1988). The programming system PRIZ. Journal of Symbolic Computation, 5(3), 359 - 375.
- ^ http://www.cs.ioc.ee/cocovila