Specifications for Intelligent Software Synthesis

Implementace jednoduchých, avšak příliš různorodých, entit ve webových aplikacích je únavná úloha, jejíž řešení se pokusíme automatizovat. Tato práce směřuje k vytvoření asistivní technologie, kdy počítače programátorům s implementací pomáhají, ale nesnaží se je plně nahradit. První otázkou je, jak počítači sdělit, co po něm chceme tak, aby taková specifikace byla jednodušší, než kdybychom to sami naprogramovali. Druhá otázka cílí na možnosti uvažování o programech – jak analyzovat to, co máme a jak odvozovat, co nám chybí. V rámci navrhovaného řešení představíme Smalldb, které formálně popisuje chování entit webové aplikace pomocí konečných automatů, avšak nesnaží se zachytit každý aspekt takové aplikace. Pro věci, které je nepraktické formálně modelovat, se ponechají dobře definované mezery a ty se následně zaplní pomocí vhodnějšího nástroje. Formální model se tak začlení jak do architektury aplikace, tak do jejího běhového prostředí, kde tvoří API mezi business logikou a prezentační vrstvou aplikace. Takto integrovaný model navíc hlídá, zda implementované chování odpovídá tomu modelovanému. Abychom zodpověděli onu první otázku, je potřeba se podívat na samotný začátek procesu vývoje aplikace a identifikovat, jaké specifikace programátoři obvykle používají při návrhu a zda jsou tyto specifikace vhodné ke strojovému zpracování. Jednou z takových specifikací jsou procesní diagramy kreslené pomocí BPMN notace. Ty použijeme jako vstup nově vytvořeného STS algoritmu, kterému architekt nakreslí, jak budou uživatelé používat danou aplikaci, a STS algoritmus odvodí implementaci v podobě Smalldb automatu. Na závěr si představíme kaskádu, která je nástrojem pro automatizované sestavování programů využívající formální modely.To relieve programmers of repetitive and tiring work on simple, yet too diverse, entities in web applications, this thesis searches for an assistive framework, where machines aid the programmers with implementing such entities. The first question to answer is how to tell the computer what we want without specifying all the details; otherwise, we could just implement the application instead. The second question is how to effectively reason about the software so that we can analyze what we have and infer what we miss. The proposed solution introduces Smalldb state machines as a formal model that describes the behavior of the entities in a web application. Such a model is not designed to cover every aspect of the application; instead, it leaves well-defined gaps for the details that are impractical to specify formally. The formal model then becomes part of the application architecture and run-time, where it provides a secure API between business logic and presentation layer; moreover, it verifies that the implementation corresponds to the model. To answer the first question, we return to the very beginning of the software development process, where we identify software specifications that programmers already use and discuss whether such specifications are sufficiently machine-friendly for automated processing. The identified BPMN business process diagrams become an input for a novel STS algorithm — a software architect draws how users will use a web application, and the STS algorithm infers the implementation in the form of a Smalldb state machine. The thesis concludes with presenting a Cascade, a machine-friendly approach to software composition based on the utilization of the formal models