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

Question

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?

Answer 1

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