От неявных к явным определениям функций

Question

Я создавал спецификации, используя неявные определения функций в VDM-SL, и это сработало очень хорошо. Теперь я хочу создать прототип спецификации, используя явные определения функций (на данном этапе никаких операций).

Один из способов сделать это - создать новый модуль, который имитирует функции, определенные в неявной спецификации, но дает им явные определения.

Я уверен, что это можно сделать, но я сомневаюсь, что это идеально. Не будет никакой связи между неявной и явной спецификацией, хотя одна является уточнением другой.

Есть ли рекомендуемый способ перехода от неявных к явным определениям функций. В долгосрочной перспективе я хочу исследовать это формально, но в первую очередь я просто хочу реализовать спецификации неявных функций, чтобы продемонстрировать спецификацию в действии.

Answer 1

Существует формальный процесс для уточнения спецификаций, хотя он довольно трудоемкий, тем более что в настоящее время для него нет инструментальной поддержки.

Если вы сохраните неявные сигнатуры типов функций и предварительные / постусловия, то явные версии "наверняка" будут уточнены, если предположить, что реализация верна для всех входных данных (в этом может помочь комбинаторное тестирование). Обратите внимание, что вы также можете дать реализацию (тело) функции, написанной в "неявном" стиле, что может упростить вещи:

f(x:nat) r:nat
== x + 1        -- This line added to the implicit spec!
pre x > 10
post r < 100