Structural synthesis of programs
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 the 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
[edit]Automatic program synthesis began in the artificial intelligence field, with software intended for automatic problem solving. The first program synthesizer was developed by Cordell Green in 1969.[4] At about the same time, mathematicians including R. Constable, Z. Manna, and R. Waldinger explained the possible use of formal logic for automatic program synthesis. Practically applicable program synthesizers appeared considerably later.
The idea of 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 the 1980s.
A recent Integrated development environment that supports SSP is CoCoViLa [9] — a model-based software development platform for implementing domain specific languages and developing large Java programs.
The logic of SSP
[edit]Structural synthesis of programs is a method for composing programs from already implemented components (e.g. from computer commands or software object methods) 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 the 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 the application of the function f. In intuitionistic logic, the function f is called a realization of this formula. A precondition can be a proposition stating that input data exists, e.g. Xi may have the meaning “variable xi has received a value”, but it may denote also some other condition, e.g. that resources needed for using the function f are available, etc. A precondition may also be 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
[edit]- ^ Maigre, Riina; Küngas, Peep et al. (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 et al. (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.
- ^ "About Cocovila". Archived from the original on 2019-07-18. Retrieved 2011-12-30.