Общее понятие верификации и валидации Примеры спецификации программ Лекция 11 Предикатное программирование
Построить спецификации 1.В списке вставить элемент x после элемента y 2. Инвертировать список 3. Удалить элемент из списка
1. В списке вставить элемент x после элемента y type T; type S = list(T); ins(S s, T x, y: ????) pre ?????????? post ????????? ;
1. В списке вставить элемент x после элемента y type T; type S = list(T); ins(S s, T x, y: S s1) post Ins(S s, T x, y, S s1) ; formula Ins(S s, T x, y, S s1) = s=nil ? s1 = s: s.car=y ? exists S s2. Ins(s.cdr,x,y,s2) & s1= y + x + s2 : exists S s2. Ins(s.cdr,x,y,s2) & s1=s.car + s2;