Почему состояние остается неизменным в небольшой семантике операционного цикла while?

9

Обычно я вижу, что в представлении структурной операционной семантики для цикла while состояние программы не изменяется:

$(while \> B \> do \>S, \sigma) \rightarrow (if \>B \> then \>S; (while \> B \> do \>S) \> else \> SKIP, \sigma)$

Для меня это не интуитивно понятно, если состояние не меняется (то есть состояние памяти остается прежним), то будет продолжать оставаться верным, и программа никогда не завершится. $B$

Может кто-нибудь объяснить, почему государство не меняется в этом правиле?

formal-languages programming-languages formal-methods operational-semantics Эль Марс
источник

Обратите внимание, что это правильно, только если мы можем предположить, что

не имеет побочных эффектов. Это не так в большинстве языков программирования.

B

$B$

Рафаэль

10

В семантике языка программирования понятие состояния программы является не смутным философским понятием, а очень точным математическим понятием. Состояние в этом небольшом шаге-операционную семантики является частичной функцией $s$

s : V a r ↪ Z

$s : \mathbf{Var} \hookrightarrow \mathbb{Z}$

который записывает значения переменных. Так что если , тогда переменная имеет значение . Состояние обязательно является частичной функцией, поскольку имеет смысл записывать только те значения переменных, которые на самом деле встречаются. $s\, x = v$ $x$ $v$

Аксиома разворачивания

⟨ while b do S, s ⟩ \Rightarrow ⟨ if b then S; while b do S else skip, s ⟩

$\langle \texttt{while}\; b\; \texttt{do}\; S,s \rangle \Rightarrow \langle \texttt{if}\; b\; \texttt{then}\; S; \texttt{while}\; b\; \texttt{do}\; S \; \texttt{else skip},s \rangle$

просто говорит нам, что мы разворачиваем цикл while в условный оператор, одна из ветвей которого содержит цикл. Никакие переменные не изменят свое значение из-за этого, и по этой причине состояние не изменяется.

Ханс Хюттель
источник

10

Состояние может измениться на последующих этапах сокращения, потому что на правой стороне

⟨ w h i l e B d o S, σ ⟩ \to ⟨ i f B t h e n (S; w h i l e B d o S) e l s e s k i p, σ ⟩

$\langle while\ B\ do\ S, \sigma \rangle \quad\rightarrow\quad \langle if\ B\ then\ ( {\color{red}{S}};\ while\ B\ do\ S )\ else\ skip, \sigma\rangle$

-loop охраняется (предваряется) с помощью . Вычисление может изменить состояние , так что условие может оценить, . $while$ $S$ $S$ $B$ $\mathsf{false}$

Мартин Бергер
источник

Итак, это означает, что изменение состояния должно быть выражено в других правилах, до которых S может быть потенциально сведен в конкретной программе?

Эль Марс

@ ElMarce Да. Я предлагаю пройти простой пример, например,

и увидеть , как это работает.

x := 2; w h i l e x > 0 d o x := x - 1

$x := 2;\ while\ x > 0\ do\ x := x - 1$

Мартин Бергер

9

Состояние не меняется , когда мы рассматриваем , чтобы решить , следует ли выполнить одну итерацию цикла, но он может изменить позже , когда мы запустим тела . Итак, в следующий раз, когда мы рассмотрим , может произойти изменение . $\sigma$ $B$ $S$ $B$ $\sigma$

Андрей Бауэр
источник

Это объяснение, хотя и является по существу правильным, не относится к тому, что представляют собой состояния (а именно функция, которая сообщает нам значения varialbes) и что означает изменение состояния (а именно, что значение по меньшей мере одной переменной изменяется).

Ганс Хюттель

Действительно, не имеет значения, что такое состояния или как они реализованы для целей моего ответа. Объяснение справедливо независимо. И более того, на самом деле неправильно говорить, что «состояния на самом деле являются функциями», потому что это только один из способов их математического моделирования. Есть и другие возможные модели. И давайте не будем путать математические модели с тем, как работает аппаратное обеспечение.

Андрей Бауэр

Но этот вопрос связан с конкретной небольшой шаговой операционной семантикой, для которой понятие состояния четко определено.

Ганс Хюттель

Я никогда не говорил, что это не так. Я просто говорю, что ваше замечание не является необходимым, потому что мое объяснение не содержит явного упоминания о том, как моделируется состояние. Возможно, вы обнаружили, что ОП не знал, что это была карта от переменных к значениям. Молодец, ваш ответ принят, а я нет. Поздравляю. Почему вы сейчас навязываете мне свой способ ответа, выше моего понимания. Почему вы чувствуете необходимость сделать мой ответ таким же, как ваш? Мой ответ имеет смысл без замечаний, которые вы считаете необходимыми. Возможно, кто-нибудь придет, когда найдет мой ответ.

Андрей Бауэр

Почему состояние остается неизменным в небольшой семантике операционного цикла while?

Ответы: