Структурированные программы - часть 2
Для x
Var через ?(x) обозначим значение переменной x в состоянии ?. Через S обозначим множество всех состояний.
Разумеется, при рассмотрении конкретной программы ? нас будут интересовать значения переменных из Var?.
Определение 7.5. Операционная семантика программы ? - это отбражение (вообще говоря, частичное) типа S
S, которое программа ? индуцирует на множестве всех состояний. Через ?(?) обозначим состояние - результат применения программы ? к состоянию ?. Оно определяется индукцией по построению программы.
- ( x := x+1)(?) = ?1, где ?1(y)=?(y) при y x, и ?1(x)=?(x)+1.
- ( x := 0)(?) = ?1, где ?1(y)=?(y) при y x, и ?1(x)=0.
- ( x := y)(?) = ?1, где ?1(z)=?(z) при z x, и ?1(x)=?(y)
- Пусть ?=?1;?2. Тогда ?(?)=(?1;?2)(?)=?2(?1(?)), при этом, если ?1(?)=? или ?1=?1(?) и ?2(?1)=?, то и ?(?)=?.
-
Пусть ?= если x = y то ?1 иначе ?2 конец. Тогда
-
Пусть ?= если x < y то ?1 иначе ?2 конец. Тогда
-
Пусть ?= пока x = y делай ?1 все. Тогда при ?(x)
?(y) ?(?)= ?, а при ?(x) = ?(y) ?(?) - это первое такое состояние ?m в последовательности состояний ?0=?, ?1=?(?0),…, ?i+1=?(?i),…, что при i m все состояния ?i определены, при i <m имеет место ?i(x) = ?i(y), и ?m(x) ?m(y). - Семантику для цикла с условием x < y определите самостоятельно (см. задачу 7.1).
Пусть ? - программа, Var? - множество ее переменных. Выделим среди эти переменных некоторое подмножество входных
переменных x1,…, xn и одну результирующую (выходную) переменную y (она может быть одной из входных). Переменные из Var? , не являющиеся входными, будем называть вспомогательными.
Содержание Назад Вперед