0

I need to verify the validity of this correctness statement by adding any intermediate assertions and inferencing , however I have never seen a statement where the last assertion is the same as the first, so am just a little lost on where to go.

ASSERT( x == y*(y+1)/2 )

y = y + 1;

x = x + y;

ASSERT( x == y*(y+1)/2 )

Mauro ALLEGRANZA
  • 94,169
algebruh
  • 27
  • This looks like proving by induction that $\sum_{i=1}^n i=\frac{n(n+1)}2$ – Andrei Nov 18 '21 at 19:36
  • "I have never seen a statement where the last assertion is the same as the first": this is an invariant, they are ubiquitous. –  Nov 19 '21 at 09:40

1 Answers1

2

This is true. Going up with the substitution rule, we have

ASSERT( x + y + 1 == (y + 1) * (y + 2) / 2 )   
y = y + 1;
ASSERT( x + y == y * (y + 1) / 2 )
x = x + y;
ASSERT( x == y * (y + 1) / 2 ).

And obviously, x + y + 1 == (y + 1) * (y + 2) / 2 is equivalent to x == (y + 1) * y / 2.