proofproof-of-correctnesshoare-logic

Using Hoare-Rules to show PRECONDITION implies POSTCONDITION in a simple program (just 2 assignments)

Using the Hoare-Rules I want to show that I can imply

{x >= 0} --> {a + y = x}

PROGRAMM

// PRECONDITION
{x >= 0}
a = x; 
y = 0;
// POSTCONDITION
{a + y = x}

Using the assignment rules I get

// PRECONDITION
{x >= 0}
{x + 0 = x}   // assignment rule
a = x; 
{a + 0 = x}   // assignment rule
y = 0;
// POSTCONDITION
{a + y = x}

To show

{x >= 0} --> {a + y = x}

therefore I need to show in a last step

{x >= 0} --> {x + 0 = x}

How can I show this or what is wrong in my proof?

Solution

  • Your reasoning is correct.

    To prove an implication formally, argue as follows:

    1. Assume the antecedent, x >= 0
    2. By Additive identity, we have x + 0 = x
    3. By implication introduction (from 1 and 2) we have x >= 0 --> x + 0 = x