--------------------------------------------------

{ x ≤ 7 }    -- logično sledi
{ x+3 ≤ 10 }
x := x + 3
{ x ≤ 10 }

--------------------------------------------------

{ x ≤ 7 }
{ x+3 ≤ 7+3 }
x := x + 3
{ x ≤ 7+3 }
{ x ≤ 10 }

--------------------------------------------------

Napiši: Program c se ne ustavi.

Odgovor: { ? } c { ? }
         [ ? ] c [ ? ]

{ false } c { false }   -- vedno velja (za vse c)

{ false } c { true  }   -- "če false in se c ustavi, potem true"
                        -- "false ∧ se_ustavi(c) ⇒ true"
                        -- "false ⇒ true"
                        -- "true"
                        -- vedno velja

{ true  } c { false }   -- "če velja true in se c ustavi, potem velja false"
                        -- "true ∧ se_ustavi(c) ⇒ false"
                        -- "se_ustavi(c) ⇒ false"   (ker true ∧ p ekvivalentno p)
                        -- "¬ se_ustavi(c)"         (ker p⇒false ekvivalentno ¬p)
                        -- "c se ne ustavi"


{ true  } c { true  }   -- ".... ⇒ true"
                        -- "true"
                        -- velja vedno

[ false ] c [ false ]   -- "če velja false, potem se c ustavi in velja false"
                        -- "false ⇒ se_ustavi(c) ∧ false"
                        -- "false ⇒ false"
                        -- "true"

[ false ] c [ true  ]   -- "če velja false, potem se c ustavi in velja true"
                        -- "false ⇒ ..."
                        -- "true"

[ true  ] c [ false ]   -- "če velja true, potem se c ustavi in velja false"
                        -- "true ⇒ se_ustavi(c) ∧ false"
                        -- "true ⇒ false"
                        -- "false"
                        -- nikoli ne velja (za noben c)

[ true  ] c [ true  ]   -- "če velja true, potem se c ustavi in velja true"
                        -- "true ⇒ se_ustavi(c) ∧ true"
                        -- "true ⇒ se_ustavi(c)"
                        -- "se_ustavi(c)"        (ker je true⇒p ekvivalentno p)
                        -- "c se ustavi"

--------------------------------------------------

{ x ≤ y }
-- logično sledi
{ x ≤ y,         x ≤ y}
-- prištejemo x, prištejemo y
{ 2 x ≤ x + y,   x + y ≤ 2 y }
-- preuredimo
{ x ≤ (x + y)/2, (x + y)/2 ≤ y }
{ x ≤ (x + y)/2 ≤ y }
s := (x + y) / 2
{ x ≤ s ≤ y }


--------------------------------------------------
DOKAŽI PRAVILNOST:

[ b ≥ 0 ]
i := 0 ;
p := 1 ;
while i < b do
   p := p * a ;
   i := i + 1
done
[ p = aᵇ ]


Najprej delna pravilnost:

{ b ≥ 0 }
i := 0 ;
{ b ≥ 0, i = 0 }
p := 1 ;
{ b ≥ 0, i = 0, p = 1 }

{ p = aⁱ ∧ i ≤ b } # INVARIANTA
while i < b do
   { p = aⁱ ∧ i ≤ b, i < b }
   { p = aⁱ ∧ i < b }   # to je easy, samo matematika
   { p*a = aⁱ⁺¹ ∧ i+1 ≤ b }
   p := p * a ;
   { p = aⁱ⁺¹ ∧ i+1 ≤ b }
   i := i + 1
   { p = aⁱ ∧ i ≤ b }
done
{ p = aⁱ ∧ i ≤ b , i ≥ b }  # logični sklep
{ p = aⁱ, i = b }           # očitno
{ p = aᵇ }

Popolna pravilnost:

Količina b-i se zmanjšuje in je ≥ 0.

Dejsto b - i ≥ 0 sledi iz i ≤ b, kar smo že preverili (je del invariante).

Količina b - i se zmanjšuje v telesu zanke:

   [ p = aⁱ ∧ i ≤ b, i < b, b - i = z ]
   [ p = aⁱ ∧ i < b, b - i = z ]
   [ p*a = aⁱ⁺¹ ∧ i+1 ≤ b, b - i = z ]
   p := p * a ;
   [ p = aⁱ⁺¹ ∧ i+1 ≤ b, b - i = z ]
   [ p = aⁱ⁺¹ ∧ i+1 ≤ b, b - (i+1-1) = z ]
   i := i + 1
   [ p = aⁱ ∧ i ≤ b, b - (i - 1) = z ]
   [ p = aⁱ ∧ i ≤ b, b - i + 1 = z ]
   [ p = aⁱ ∧ i ≤ b, b - i = z - 1]
   [ p = aⁱ ∧ i ≤ b, b - i = z - 1 < z]
   [ p = aⁱ ∧ i ≤ b, b - i < z ]