Структурный синтез программ
Структурный синтез программ (ССП) — это особая форма (автоматического) синтеза программ , основанная на исчислении высказываний . Точнее, он использует интуиционистскую логику для настолько детального описания структуры программы, что программа может автоматически состоять из таких частей, как подпрограммы или даже компьютерные команды. Предполагается, что эти части реализованы правильно, поэтому проверка правильности этих частей не требуется. SSP хорошо подходит для автоматического составления услуг. [1] для сервис-ориентированных архитектур и синтеза больших программ моделирования . [2] [3]
История
[ редактировать ]Автоматический синтез программ начался в области искусственного интеллекта с программного обеспечения, предназначенного для автоматического решения проблем. Первый программный синтезатор был разработан Корделлом Грином в 1969 году. [4] Примерно в то же время математики, в том числе Р. Констебль , З. Манна и Р. Вальдингер , объяснили возможность использования формальной логики для автоматического синтеза программ. Практически применимые программные синтезаторы появились значительно позже.
Идея структурного синтеза программ была представлена на конференции по алгоритмам в современной математике и информатике [5] организован Андреем Ершовым и Дональдом Кнутом в 1979 году. Идея взята из Г. Полиа о решении задач. известной книги [6] Метод разработки плана решения задачи в SSP был представлен как формальная система . Правила вывода системы были реструктурированы и логически обоснованы Г. Минцем и Э. Тюгу. [7] в 1982 году. Инструмент программирования ПРИЗ. [8] использующий SSP, был разработан в 1980-х годах.
Недавней интегрированной средой разработки , поддерживающей SSP, является CoCoViLa. [9] — основанная на моделях платформа разработки программного обеспечения для реализации предметно-ориентированных языков и разработки больших программ на Java .
Логика SSP
[ редактировать ]Структурный синтез программ — это метод составления программ из уже реализованных компонентов (например, из компьютерных команд или методов программного объекта), которые можно рассматривать как функции. Спецификация синтеза дается в интуиционистской логике высказываний путем записи аксиом о применимости функций. Аксиома о применимости функции f — это логическое следствие.
- Икс 1 ∧ Икс 2 ∧ ... ∧ Икс м → Y 1 ∧ Y 2 ... Y n ,
где X 1 , X 2 , ... X m - предусловия , а Y 1 , Y 2 , ... Y n - постусловия применения функции f . В интуиционистской логике функция f называется реализацией этой формулы. Предварительным условием может быть утверждение, утверждающее, что входные данные существуют, например, X i может иметь значение «переменная x i получила значение», но оно может также обозначать какое-то другое условие, например, что ресурсы, необходимые для использования функции f , доступны, и т. д. Предусловие может также быть импликацией той же формы, что и приведенная выше аксиома; тогда это называется подзадачой. Подзадача обозначает функцию, которая должна быть доступна в качестве входных данных при функции f применении . Сама эта функция должна быть синтезирована в процессе SSP. В данном случае реализацией аксиомы является функция более высокого порядка , т. е. функция, которая использует в качестве входных данных другую функцию. Например, формула
- ( состояние → nextState ) ∧ InitialState → результат
может указать функцию более высокого порядка с двумя входными параметрами и выходным результатом . Первый вход — это функция, которую необходимо синтезировать для вычисления nextState из состояния , а второй вход — InitialState . Функции высшего порядка придают SSP общность: любая управляющая структура, необходимая в синтезируемой программе, может быть предварительно запрограммирована и затем автоматически использована с соответствующей спецификацией. В частности, последняя представленная здесь аксиома представляет собой спецификацию сложной программы – механизма моделирования динамических систем на моделях, где nextState можно вычислить на основе состояния системы.
Ссылки
[ редактировать ]- ^ Мегре, Риина; Кюнгас, Пип и др. (2009). Динамический синтез сервисов на основе крупных сервисных моделей федеративной правительственной информационной системы. Международный журнал достижений в области интеллектуальных систем, 2 (1), 181–191.
- ^ Коткас, Вахур; Оямаа, Андрес; Григоренко, Павел и др. (2011). CoCoViLa как многофункциональная платформа моделирования. В: SIMUTOOLS 2011 — 4-я Международная конференция ICST по инструментам и методам моделирования: 21–25 марта — Барселона, Испания: Брюссель: ICST, 2011, [1–8].
- ^ Гроссмидт, Гуннар; Харф, Мейт (2009). COCO-SIM - объектно-ориентированная многополюсная среда моделирования и моделирования гидроэнергетических систем. Часть 1: Основы. Международный журнал гидроэнергетики, 10 (2), 91–100.
- ^ Грин, Корделл (1969) Применение доказательства теорем к решению проблем. Материалы Международной совместной конференции по искусственному интеллекту. Дональд Э. Уокер и Льюис М. Нортон, редакторы, издательство Gordon and Breach Science Publishers, Нью-Йорк, Нью-Йорк, 219–239.
- ^ Тюгу, Э.Х. (1981). Структурный синтез программ. В: Алгоритмы в современной математике и информатике: Труды, Ургенч, Узбекская ССР, 16–22 сентября 1979 г.: Ершов А.П.; Кнут, Д.Э. (ред.) Берлин: Springer, 1981 (Конспекты лекций по информатике; 122), 290–303.
- ^ Полиа, Г. (1957) Как решить проблему. Издательство Принстонского университета.
- ^ Минц, Г.; Тюгу, Э. (1982). Обоснование структурного синтеза программ. Наука компьютерного программирования, 2 (3), 215–240.
- ^ Минц, Г.; Тюгу, Э. (1988). Система программирования ПРИЗ. Журнал символических вычислений, 5 (3), 359–375.
- ^ «О Коковиле» . Архивировано из оригинала 18 июля 2019 г. Проверено 30 декабря 2011 г.