Интернет магазин китайских планшетных компьютеров



Компьютеры - Логика Хоара - Примеры

23 января 2011


Оглавление:
1. Логика Хоара
2. Частичная и полная корректность
3. Примеры



Пример 1
 \{ x+1 = 43 \}\ y:=x+1\ \{ y = 43 \} \! — на основании аксиомы присваивания.
Поскольку , на основании правила вывода получаем:
\{x=42\}\ y:=x + 1\ \{y=43 \land x=42\}\!
Пример 2
\{x + 1 \leq N \}\ x:= x+1\ \{x \leq N\}\ \! — на основании аксиомы присваивания.
Если x и N целые, то  \implies, и на основании правила вывода получаем:
\{x < N \}\ x:=x+1\ \{x \leq N\}\ \!


Просмотров: 3672


<<< Логика в информатике
Лямбда-исчисление >>>