------------------------------- Assign
    X > 0 /\ X = 0 ==> X+1 > 0     { X+1 > 0 } X ::= X+1 { X > 0 }
------------------------------------------------------------------ Consequence
    { X > 0 /\ X = 0 } X ::= X+1 { X > 0 }
------------------------------------------------- While
{ X > 0 }  WHILE X = 0 DO X ::= X+1 END { X > 0 }




--------------------------------- SMT
X = Y + Z /\ Y > 10 ==> X = Y-1 + Z+1    ----A
      { X = Y-1 + Z+1 } Y := Y-1 { X = Y + Z+1}
C----------------------------------------------  ------------------------------- Assign
{ X = Y + Z /\ Y > 10 } Y := Y-1 { X = Y + Z+1}  { X = Y + Z+1 } Z ::= Z+1 { X = Y + Z }
    --------------------------------------------------------- Seq
    { X = Y + Z /\ Y > 10 } Y := Y-1; Z ::= Z+1 { X = Y + Z }
----------------------------------------------------------------- While
{ X = Y + Z } WHILE Y>10 DO Y := Y-1; Z ::= Z+1 END { X = Y + Z }





             ------------------------ Skip
             { True /\ True } SKIP { True }
             -------------------------------------------
P ==> True   { True } WHILE True DO SKIP END { P /\ ~True }   rue /\ ~True ==> Q
------------------------------------------------------------------- Consequence
  { P } WHILE True DO SKIP END { Q }




Loop entered        { G /\ G } c { G }     Loops
-----        ----------------------------------
P ==> G      { G } WHILE G DO c END { G /\ ~G }   G /\ ~G ==> Q
---------------------------------------------------------------- Consequence
              { P } WHILE G DO c END { Q }



{ fun h' -> h' X + 1 <= 5 }
{ fun h' -> (eval_aexp h' (X+1)) <= 5 }
{ fun h' -> (update h' X (eval_aexp h' (X+1))) X <= 5 }
      X ::= X + 1
{ fun h -> h X <= 5 }




{ wlp c1 (wlp c2 q) } c1 {wlp c2 q}         {wlp c2 q}  c2 { q }
----------------------------------------------------------------
             { wlp c1 (wlp c2 q) } c1; c2 { q }