Program Synthesis

Enter a topic name to show or a new topic name to create; then press Enter

.

Summary

Derivation of a program from a specification.

Approaches

Formal Methods

Formal method approaches use mathematically based techniques for the specification. Many specification formalisms are possible such first-order logic, pre/post conditions and algebraic specifications. Program derivation is considered to be a theorem proving task using deductive synthesis. Program synthesis by inductive synthesis is also possible using specification by examples.

http://en.wikipedia.org/wiki/Formal_methods

http://en.wikipedia.org/wiki/Logic_programming

http://en.wikipedia.org/wiki/Predicate_calculus

Pro's

- highly rigorous

- good for verification

- excellent where safety is critical

Con's

- need good mathematical skills

- limited scope of application

Compositional

The notion behind compositional program synthesis is that software development is best described as the process of adding capabilities to an existing structure. The goal is to reduce software development costs by treating software modules as incremental, evolutionary enhancements. A successful CPS effort requires a library of composable elements and a coherent set of composition rules.

http://www.pnambic.com/CPS/

Model-based

Artifacts of a program and their relationships are modeled at a highly abstract level (non platform specific). Program synthesis involves a series of transformations which lowers the abstraction until it is executable on a particular platform. This is called transformational synthesis or structural synthesis.

Modelling can be approached using either a general modelling language like UML 2 or domain specific languages.

Note that are also procedural DSL's that should not be confused with DSL's for high level specification.

Aspect-oriented

Aspect-oriented approaches work to address a greater seperation of concerns at a language level focusing on the modularization and encapsulation of cross-cutting concerns. It's primarily an evolution of object-oriented programming. Programs are synthesised by weaving aspects together.

Schema-based

Program synthesis occurs by recursively apply schema's to gradually refine a specification into executable code.

http://ic.arc.nasa.gov/people/edenney/papers/ontologies.pdf

Are these really alternative approaches?

Generative

Generative programming is a more sweeping approach which is characterised by modelling families of applications and then assembling specific instances of them using any of the previous approaches.

http://www.program-transformation.org/Transform/GenerativeProgramming

Feature-oriented programming

Intentional programming.

?

PhD Topics

 Model-based software synthesis
 type theory
 compositional reasoning

Follow-up papers

http://www.csl.sri.com/users/ruess/papers/KBSE95/index.html

http://www.cs.berkeley.edu/~bodik/cs294/description.html

http://www2.info.ucl.ac.be/people/YDE/Papers/lpsynt_jsc93.pdf

http://www.cs.cmu.edu/%7Ejinghai/papers/thesis.pdf

http://www.intellektik.informatik.tu-darmstadt.de/~bibel/