Câu 10: Trình bày hệ tiên đề Hoare.

Hệ tiên đề 1(H1) : tính chất của phép gan :

{P}  x:=E {Q}.

{ P è Q[x/E] }

+Điều kiện đủ để Q đúng sau khi thực hiện phép gán x=E là (E là một biểu thức) trước khi thực hiện phép gán ta phải có : Q[x/E] là đúng ,Q[x/E] là phép thế mọi x trong Q bằng E.

+Điều kiện đủ để có Q sau khi thực hiện phép gán x=E là trước đó ta phải có P suy diễn được ra Q[x/E].

Hệ tiên đề 2(H2) : tính chất của dãy thao tác:

Nếu {P} T1 {Q} và {Q} T2 {R} thì {p} T1 ; T2 {R}

Hệ tiên đề 3( H3) : Tính chất của cấu trúc rẽ nhánh :

+ Dạng 1:

   Nếu {P ,C} A {Q} và {P , !C} è{Q} thì {P} if C then A {Q}

+Dạng 2 :

   Nếu {P ,C} A {Q} và {P , !C} B {Q} thì  {P}  if  C  then  A  else B {Q}.

Hệ tiên đề 4 ( H4) :  Tính chất của vòng lặp với điều kiện trước :

+ Dạng 1:    While B do S  { ! B }

+Dạng 2 : Nếu  { P và B} S {P} thì {P}

                     While B do S {P}

                       {P và !B}

Chú ý dạng 2 của hệ tiên đề 4 : đó là tính chất hết sức quan  trọng của vòng lặp.Nếu P là bất biến với S theo điều kiện B (Nghĩa là nếu P và B đúng sau khi thực hiện S ta thu được P đúng) thì P sẽ bất biến đối với chính vòng lặp.