Доказательство правильности представления данных
Правильность представления данных.
Доказательство правильности представления данных
Переход от абстрактной программы к конкретной
Метод перехода от абстрактной программы к конкретной, а также доказательство правильности такого перехода.
В абстрактной программе нет типов данных.
Записывается программа в общем виде и делается переход к конкретной программе, доказывается, что она соответствует абстрактной программе.
Абстрактная программа намного короче конкретной.
t- абстрактная переменная, ее тип Т. (например объект типа множества)
с1, с2, …, сn – конкретное представление t.
Рекомендуемые материалы
Операции с t1 возможны следующие: Р1, Р2, …, Рm.
Конкретное представление
Class T;
Begin
Описание с1, с2, …, сn;
Procedure P1 (формальные параметры); Q1;
…
Procedure Pm (формальные параметры); Qm;
Q (призвание начальных значений с1, с2, …, сn)
End
Qi – тело Pi процедуры
Для описания переменной
Var t1, t2, … : T
t2.Pj – вызов Pj процедуры для t2
Опишем множество целых чисел.
Class НМЦ;
Begin
Var
m: integer;
b: array[0..99] of integer;
Обратите внимание на лекцию "3. Внемашинное информационное обеспечение".
proc добавить(value i:integer);
Proc содержит(value l: integer; result is: boolean);
Proc удалить(value i:integer)
m:=0;
end