I've written a function that gets a permutation and checks if that permutation can be reached using a stack from an input sequence which is <1,2,3,...,n>. (we take elements from left)
For example: if we have an input sequence, then if the function gets these permutations:
<4,3,2,1> - Returns true since we can push (1) push (2) push (3) push (4) and then pop (4) pop pop pop to get this permutation.
<4,3,1,2> - Returns false since this permutation cannot be reached (2 will always be above 1 in the stack after reaching 4,3).
The algorithm looks something like this in pseudocode:
I've referred to the permutation we're checking by P, and the <1,2,3,...,n> sequence by In(input).
The empty stack I'm using will be S.
While (In is not empty) i = 0 Take In leftmost element store it in x (1 then 2 then 3,...) if (x == P[i]) i = i + 1 // i can be printed by push pop so we keep going while(S is not empty) x = pop(S) if (x == P[i]) i = i + 1 // x is the next number in the permutation else push(x) // x isn't the next number so we keep it in stack for later break else push(x) if (S is not empty AND i = n+1) return TRUE else return false
The idea is to keep taking numbers from our input sequence (In) until we reach the next permutation number (P[i]), once we reach it we check if the next one can be found in the stack before checking the next input numbers (they will be sorted such that the biggest will be on top of the stack, so if it's lower value than the top we can't really reach it, and if it's higher value then we will reach it in the input sequence).
Now what I'm trying to do is to prove the correctness of this algorithm, for that I know I need to write some loop invariants for my loops, I've tried to think of my goal, which is to check if a permutation can be reached using a stack, if the stack is not empty at the end, then we got stuck and the permutation can't be reached, just like <4,3,1,2>.
My attempt for loop-variant for the outer loop (
while(In not empty)):
At the start if each iteration, the elements P[0...i-1] (As of all the elements of the permutation until the one P[i] we're looking at now), are either reached in the permutation (Pushed and popped - just like 4 in <4,3,1,2> when we're looking at 3, it would have been reached by push push push push pop), OR they're inside the stack.
Now if this worked, I would've been done since at the end if the stack isn't empty, then the permutation cannot be created, but when I looked in the inner loop, I still go into the stack to check, so the elements P[1...i-1] are really reached again sometimes and that ruined my plans, and I've been stuck trying to come up with another loop invariant or fixing this one.
I would appreciate any help and feedback, Thanks in advance.