Аксиоматическая семантика команд присваивания, ввода, вывода, последовательной композиции. Вспомогательные правила вывода. | MetodPro.ru

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

Аксиоматическая семантика команд присваивания, ввода, вывода, последовательной композиции. Вспомогательные правила вывода.


49. Аксиоматическая семантика команд присваивания, ввода, вывода, последовательной композиции. Вспомогательные правила вывода.
Аксиоматическая семантика чаще всего используется для док-ва правильности программ.
Спецификация команды:  {PRE} C {POST}
PRE и POST – логические формулы. POST должно быть истинно по завершении команды, при условии того, что перед выполнением было истинно предусловие. PRE и POST – спецификации команды C. Программа является частично корректной по отношению к её предусловию и постусловию, если она начав работу в состоянии, для которого истинно предусловие, в случае завершения даст результат, для которого постусловие истинно.
Команда присваивания
Пример1
{k=5} k := k+1 {k=6}
{k=6} – постусловие
{k+1=6} - делаем подстановку k+1 вместо k
{k=5} - после упрощения получим предусловие
Пример2
{a>0} a := a-1 {a>=0}
{a>=0} – постусловие
{a-1>=0} - делаем подстановку a-1 вместо a
{a>=1} - упростили
{a>0} – считаем, что a-целое, тогда {a>=1} = {a>0}
Семантика команды присваивания: {P[V->E]}  V := E  {P}
Если утверждения представлены в форме предикатов то: {P(E)}  V := E  {P(V)}
Для примера 3 доказательство можно представить так:
{a>0} -> {a>=1} -> {a-1>=0} = {P(a-1)} - ввели обозначение      a := a-1
 {a>=0} = {P(a)}
Команды ввода-вывода
Файл: [1,2,3]
Конкатенация: [1,2,3] [4] => [1,2,3,4].
Семантика команды ввода:  {IN=[k]L & P[V->k]}  read V {IN=L & P}
Семантика команды вывода:   {OUT=L & E=k & P}  write E {OUT=L[k] & E=k & P}
Последовательная композиция команд
<числитель>{P}  С1  {Q} ,     {Q}  С2  {R}</числитель>
<знаменатель>{P}  C1; С2  {R} </знаменатель>
Вспомогательные команды вывода
<числ>{P}  С  {Q} , Q->R </числ><знам>{P} C {R} </знам> - ослабить
<числ> P->Q,  {Q}  С  {R} </числ><знам>{P} C {R} </знам> - усилить
<числ>{P1}  С  {Q1}, {P2}  С  {Q2} </числ><знам>{P1&P2} C {Q1 & Q2} </знам> - объединить по И
<числ>{P1}  С  {Q1}, {P2}  С  {Q2} </числ><знам>{P1 || P2} C {Q1 || Q2} </знам> объединить по ИЛИ



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

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