Аксиоматическая семантика команды while. | MetodPro.ru

Реклама на сайте

Аксиоматическая семантика команды while.


50.Аксиоматическая семантика команды while.
<числ>{P & B}  С  {P} <числ/>
<знам>{P}  while B do C {P & !B} <знам/>
P – инвариант цикла. Он должен быть истиной в начале, сохранять истинность в каждом витки и быть истиной в конце.
Доказательство корректности цикла имеет 3 части:
1 Доказать правильности инициализации
2 Доказать неизменность инварианта
3 Доказать, что из инварианта и условия выхода из цикла следует результирующее утверждение.
Инвариант должен включать отношение между переменными, изменяющимися в цикле, которое не изменялось бы в течении цикла.
Пример
{N>=0}
  k := N; f := 1;
  while k>o do
    begin {инвариант цикла}
      f := f*k;
      k := k-1
    end;
{f=N!}
Можно увидеть инвариант: {f*k!=N! & k>=0}
Истинность инварианта на входе в цикл
N>=0} ->         // добавим тавтологию N!=N!, которая истинна для N>0
{N!=N! & N>= 0}
  k:= N;
{k!=N! & k>= 0} ->  // добавим сомножитель 1
{1*k!=N! & k>=0}
  f:=1
{f*k!=N! & k>=0}
Истинность инварианта на каждом витке цикла
{f*k!=N! & k > 0} ->         // это P & B
{f*k*(k-1)!=N! & k>0}   // по определению факториала
  f:= f*k;
{f*(k-1)!=N! & k>0} ->
{f*(k-1)!=N! & k-1>=0} 
  k:=k-1
{f*k!=N! & k >= 0}
Истинность инварианта по завершении цикла
{f*k!=N! & k >= 0 & !(k>0)} ->
{f*k!=N! & k >= 0 & k<=0} ->
{f*k!=N! & k=0} ->
{f=N! & k=0} -> {f=N!}



Методические пособия

  • Системы автоматизированного проектирования
  • Социология молодёжи
  • Общая социология
  • Криптография
  • Проектирование трансляторов
  • Компьютерная графика
  • Моделирование систем
  • Информационная безопасность
  • Теория вычислительных процессов
  • Логические основы искусственного интелекта
  • Проектирование распределённых информационных систем