Сложились методы программирования обладающие свойством доказательности и не теряющие это точное, накопленное знание [Поттосин 1997]. Три. таких метода соответствуют уже исследованным генетическим подходам, с учетом формальных, математических спецификаций.
Формальное синтезирующее программирование использует математическую спецификацию - совокупность логических формул. Существуют две разновидности синтезирующего программирования:
- логическое, в котором программа извлекается как конструктивное доказательство из спецификации, понимаемой как теорема;
- трансформационное, в котором спецификация рассматривается уравнение относительно программы и символическими преобразованиями превращается в программу.
- формальное сборочное программирование использует спецификацию как композицию уже известных фрагментов.
- формальное конкретизирующее программирование использует такие походы, как смешанные вычисления и конкретизацию по аннотациям.
Одной из наиболее интересных современных работ в области формальных генетических подходов является В-технология [Abrial 1996]. На ее основе была осуществлена разработка системы управления парижским метрополитеном “МЕТЕОR”.