SEAMLESS Framework
Objectives
Formal correctness and conformance with user needs are criteria to assess the quality of software. Automatic software generation from formal descriptions of user requirements by elaborating algorithms and programs from constructive proofs is a promising approach to achieve correct software. The deductive approach covers only parts of automated development processes due to the incompleteness of uniform proof procedures and the inherent exponential proof complexities. Experiences gathered so far from automatically solved complex algorithmic problems, suggest that computer-assisted construction of solutions for non-trivial problems in reasonable times involves - besides programming knowledge and the guidance by abstract principles - comprehensive domain specific, heuristic and strategic knowledge. One of the major problems is modeling in advance knowledge and requirements in a non-ambiguous, complete, correct, and adequate way. Thus, specifications are subject to continual changes.
The intent of the SEAMLESS approach is to provide efficient generic methods and knowledge representation technics for algorithm and software synthesis from examples within a logical framework. The requirements taken into account consist of functional properties as well as further constraints, eg. the worst-case complexity of synthesized algorithms. SEAMLESS takes the view that the whole synthesis knowledge should be organized as an easily extensible family of re-usable encapsulated knowledge units which are interacting by well-defined interfaces and are hierarchically organized. A synthesis process is perceived as a non-linear, spiraling knowledge acquisition process, subdivided into the phases »Specification, Experimentation, Abstraction, Modification, based upon Logic, Efficiency and Structure for Synthesis (SEAMLESS).« In each step, knowledge bases are taken and transformed by applying generic methods. Thus, we stress the incremental nature of software development. This contrasts with the traditional approaches, usually based on deductive first order logic or metalogical frameworks. Although these are intended to be generally applicable, they neglect the need for representation of (meta-)knowledge and its re-use oriented management. Thus, in most cases, the domain modeling and the derivation of methods remain ad-hoc processes, which have to be done manually from scratch in each case.
Approach
The formal foundation is a multi-layer architecture for knowledge representation within the logic programming paradigm. It allows to apply a uniform notation and a coherent concept for the seamless modeling of heterogenous forms of synthesis knowledge, eg. domain data or software components, and supporting reasoning tasks, eg. knowledge acquisition, software construction or program optimisation. Three abstraction layers - each of them is subdivided into data types, declarative theories, and executable specifications are introduced. The layers refer to the modeling of domain knowledge, generic domain abstractions, ie. schemas and problem solving knowledge, and the organization of distributed knowledge sources, eg. program components, respectively. The interaction between object layers and metalayers and different representation formats is realized by viewpoints, which entail information to dynamically instantiate abstract domain schemas by concrete domain theories. Generic methods are metatheorems which are derived from declarative generic theories. Problems to be solved are stated as theorems to be proven and submitted as queries. Constructive solutions are computed by evaluating generic methods.
Status
Within the SEAMLESS framework correct and declarative or operational specifications of data types, optimisation rules for logic programs, mathematical domain knowledge, and generic methods were devised. Based on these theoretical results, the current implementation provides – among others – the following services.
Data types and knowledge bases:
- Canonical terms and term rewrite rules efficiently implementing directed acylic graphs, classes of isomorphic graphs, graph operations and hierarchically organized graph concepts within a horn clause framework;
- Comprehensive knowledge base, entailing knowledge on partial-order sorting problems, its complexities and algorithms to solve subproblems;
- Metalogic extensions, which allow to deal with programs and theories as typed data in horn clause programs, providing mechanism for dynamic binding, operations to transform and construct theories, data types to classify aggregated theories and contextual proving;
Generic methods:
- Theory formation by abstraction, specialisation and generalisation, given positive and negative ground atoms and a concept lattice;
- Synthesis from examples based on an extended divide-and-conquer method;
- Extraction of executable programs from proof terms
Context modes:
- Knowledge acquisition , based on deductive analysis of search processes and intermediately or finally solved cases. Derived knowledge is stored within dynamic libraries;
- Re-use of previously acquired knowledge: proofs, control knowledge, synthesised lemmata and hypotheses.
SEAMLESS allows to develop new generic methods by devising generic theories and deriving methods as metatheorems. A user develops a problem specification by instantiating generic theories through views and employing already defined data types. Complex problems are solved in an incremental process by creating, extending and refining knowledge bases.
Generic Realization, Experimental Results and XML Document Synthesis
SEAMLESS is implemented in Prolog and runs on various platforms. The system integrates a component for graph layout which is used to visualize synthesis artifacts at different levels of abstraction in an incremental and composite way applying standard visualization algorithms. This architecture provides desirable features as flexibility and re-usability.
SEAMLESS was applied for the discovery of a previously unknown, complex mathematical algorithm in the domain of partial-order sorting. Search complexities were tackled by extended strategic knowledge, which was implemented as annotated expert knowledge and automatically augmented at runtime by machine learning procedures.