1

I am trying to study for a test in my programming language concepts class.

I am trying to understand how to solve this problem. Our professor said we don't need to use formal notation to prove the problem as long as he can understand what we are saying.

I missed the lecture where he solved the problem and I'm having a very hard time finding resources to help me solve it on my own.

Would be so thankful for an explanation.

Problem

Use axiomatic semantics to prove that the postcondition is true following the execution of the program assuming the precondition is true

Precondition: n ≥ 0 and A contains n elements indexed from 0

bound = n;
while (bound > 0) {
  t = 0;
  for (i = 0; i < bound-1; i++) {
    if (A[i] > A[i+1]) {
      swap = A[i];
      A[i] = A[i+1];
      A[i+1] = swap;
      t = i+1;
    }
  }
  bound = t;
}


Postcondition: A[0] ≤ A[1] ≤ ...≤ A[n-1]
Community
  • 1
yako
  • 311

1 Answers1

0

Assume you have a list of number $A=[a_1,a_2,...,a_n]$, then this program is supposed to shuffle all the $a_i$'s in to the right order.

How does work?

Gonna make this short

bound = n;

Decides the stopping point for when the program starts sorting.

while (bound > 0) { t = 0;

Starts a while loop and then sets t=0 (obvious but important)

for (i = 0; i < bound-1; i++) { if (A[i] > A[i+1]) { swap = A[i]; A[i] = A[i+1]; A[i+1] = swap; t = i+1; } }

Drags the largest number that isn't in the right place to the right place.

bound = t;

t- number such that everything above A[t] is in the right position (Including A[t]).

(Can also be defined as the new position of the largest number that wasn't in the right place)

[The for loop makes the above statements true.]

So bound = t; just gives us how much we have to sort left.

Program then goes back to the while loop.

Run through a couple examples to see if what I am saying is true.

user160110
  • 2,700
  • 17
  • 27