Вікіпедія

Логіка Гоара: відмінності між версіями

Інтерактивний перегляд історії
[неперевірена версія][неперевірена версія]
Наступне редагування →
Вилучено вміст Додано вміст
ВізуальнийВікірозмітка
Створена сторінка: '''Логіка Хоара''' (також відома як '''Флойда-Хоара''') - це формальна система з множиною лог...
 
Рядок 20:
 
:<math> \frac{}{\{P\}\ \textbf{skip}\ \{P\}} \!</math>
{{пишу}}
<!--
===Assignment axiom schema===
 
=== Аксіома про присвоєння ===
The assignment axiom states that after the assignment any predicate holds for the variable that was previously true for the right-hand side of the assignment:
Аксіома про присвоєння каже що після присвоєння для змінної виконується предикат, який виконувався для правої частини оператора присвоєння:
 
:<math> \frac{}{\{P[E/x]\}\ x:=E \ \{P\} } \!</math>
 
HereТут <math>P[E/x]</math> denotesпозначає the expressionвираз ''P'' inу whichякому allвсі [[Freeвільна variables and bound variablesзмінна|freeвільні occurrenceвходження]]s of the variableзмінної ''x'' have been replaced withбули theзамінені expressionвиразом ''E''.
 
TheАксіома assignmentпро axiomприсвоєння meansозначає thatщо the truth ofістинність <math>\{P[E/x]\}</math> isеквівалентна equivalent to the after-assignment truth ofістинності <math>\{P\}</math> після присвоєння. ThusТобто wereякщо <math>\{P[E/x]\}</math> ''true''була priorістинна toдо the assignment, by the assignment axiomприсвоєння, thenто <math>\{P\}</math> wouldбуде beпісля. ''true''І subsequent to which. Converselyнавпаки, wereякщо <math>\{P[E/x]\}</math> ''false''була priorхибною toдо theприсвоєння, assignment statement,то <math>\{P\}</math> mustтеж thenмає beбути ''false''хибною consequentlyпісля.
 
Приклади правильних трійок:
Examples of valid triples include:
 
:*<math>\{x+1 = 43\}\ y:=x + 1\ \{ y = 43 \}\!</math>
:*<math>\{x + 1 \leq N \}\ x := x + 1\ \{x \leq N\}\ \!</math>
 
The assignment axiom proposed by Hoare ''does not apply'' when more than one name may refer to the same stored value. For example,
 
=== Правило композиції ===
:<math>\{ y = 3\} \ x := 2\ \{y = 3 \}</math>
Правило композиції застосовується до послідовно виконуваних програм ''S'' та ''T'', де ''S'' виконується до ''T'' і записується ''S;T''.
 
is not a true statement if ''x'' and ''y'' refer to the same variable, because no precondition can cause ''y'' to be 3 after ''x'' is set to 2.
 
===Rule of composition===
 
Hoare's rule of composition applies to sequentially-executed programs ''S'' and ''T'', where ''S'' executes prior to ''T'' and is written ''S;T''.
 
:<math> \frac {\{P\}\ S\ \{Q\}\ , \ \{Q\}\ T\ \{R\} } {\{P\}\ S;T\ \{R\}} \!</math>
 
Наприклад, розглянемо такі два присвоєння:
For example, consider the following two instances of the assignment axiom:
 
:<math>\{ x + 1 = 43\} \ y:=x + 1\ \{y =43 \}</math>
 
та
and
 
:<math>\{ y = 43\} \ z:=y\ \{z =43 \}</math>
 
 
By the sequencing rule, one concludes:
З правила композиції:
 
:<math>\{ x + 1 = 43\} \ y:=x + 1; z:= y\ \{z =43 \}</math>
 
=== Правило умови ===
===Conditional rule===
З трійки для умовного оператора можна вивести дві трійки: одну для випадку істинності умови, іншу для її хибності:
 
:<math>\frac { \{B \wedge P\}\ S\ \{Q\}\ ,\ \{\neg B \wedge P \}\ T\ \{Q\} }
{ \{P\}\ \textbf{if}\ B\ \textbf{then}\ S\ \textbf{else}\ T\ \textbf{endif}\ \{Q\} } \!</math>
 
=== Правило висновків ===
===Consequence rule===
Передумову та/або постумову можна замінити, якщо для них виконуються певні [[імплікація|імплікації]]:
 
:<math>
\frac { P^\prime \rightarrow\ P\ ,\ \lbrace P \rbrace\ S\ \lbrace Q \rbrace\ ,\ Q \rightarrow\ Q^\prime }
Рядок 73 ⟶ 66:
\!</math>
 
===While ruleПравило While===
 
:<math>\frac { \{P \wedge B \}\ S\ \{P\} }
Рядок 79 ⟶ 72:
\!</math>
 
HereТут ''P'' is the [[loopінваріант invariantциклу]].
 
=== Правило While для тотальної коректності ===
===While rule for total correctness===
 
::<math>
Рядок 87 ⟶ 80:
{ [P]\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ [\neg B \wedge P] }
\!</math>
В цьому правилі на додачу до інваріанта циклу, також доводять завершуваність додаванням [[варіант циклу|варіанта циклу]] (тут ''t''), чиє значення строго спадає згідно з [[:en:well-founded relation]] протягом кожної ітерації. Через те що відношення "&lt;" well-founded, кожна ітерація циклу перелічується спадними членами скінченного [[ланцюг (теорія порядку)|ланцюга]]. Також зауважте, що тут для позначення тотальної коректності використовуюються квадратні дужки, тобто завершуваності. (Це одне з можливих позначень тотальної коректності.)
 
== Приклади ==
In this rule, in addition to maintaining the loop invariant, one also proves [[termination proof|termination]] by way of a term, called the [[loop variant]], here ''t'', whose value strictly decreases with respect to a [[well-founded relation]] during each iteration. Note that, given the invariant ''P'', the condition ''B'' must imply that ''t'' is not a [[minimal element]] of its range, for otherwise the premise of this rule would be false. Because the relation "<" is well-founded, each step of the loop is counted by decreasing members of a finite [[chain (order theory)|chain]]. Also note that square brackets are used here instead of curly braces to denote [[total correctness]], i.e. termination as well as partial correctness. (This is one of various notations for total correctness.)
 
==Examples==
 
:{|style="text-align:left"
|bgcolor="#C0C0C0" colspan=4|'''ExampleПриклад 1'''
|-
|<math>\{x+1 = 43\}\!</math>
|<math>\ y:=x + 1\ \!</math>
|<math>\{ y = 43 \}\!</math>
|(Аксіома присвоєння)
|(Assignment Axiom)
|-
|
Рядок 108 ⟶ 100:
|<math>\ y:=x + 1\ \!</math>
|<math>\{y=43 \land x=42\}\!</math>
|(Правило висновків)
|(Consequence Rule)
|-
|bgcolor="#C0C0C0" colspan=4|'''ExampleПриклад 2'''
|-
|<math>\{x + 1 \leq N \}\!</math>
|<math>\ x := x + 1\ \!</math>
|<math>\{x \leq N\}\ \!</math>
|(Аксіома присвоєння)
|(Assignment Axiom)
|-
|
Рядок 125 ⟶ 117:
|<math>\ x := x + 1\ \!</math>
|<math>\{x \leq N\}\ \!</math>
|(Правило висновків)
|(Consequence Rule)
|}-->
 
== Дивіться також ==
Отримано з https://uk.wikipedia.org/wiki/Логіка_Гоара