What loop invariant can be used for this loop? (Algorithm to check if a sequence is stack permutable)

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.

• If you have figured out an answer, you can post it. Otherwise, are you still interested in an answer? Apr 23 at 14:11
• @JohnL. I'm still interested in an answer, the maximum I've reached is convincing myself why it works, but couldn't come up with a loop invariant that could prove the correctness of the algorithm. Apr 23 at 17:36
• I will write an answer today. Here is a spoiler. It will correspond to how you have convinced why it work probably. Apr 23 at 17:39
• Got sidetracked. Tomorrow then. Apr 24 at 4:06
• @JohnL. No worries! Whenever you have time Apr 24 at 19:37

This question is interesting in the sense that although people might convince themselves that the "obvious" algorithm is correct, it may not be obvious to find a good loop invariant.

The Basic Idea

Your algorithm is, in fact, simulating the possible sequence of actions that produces a given stack-permutable sequence. Given a stack-permutable sequence, there is only one sequence of actions to produce it essentially. If your algorithm takes the only possibly-successful actions upon each input number, it must be correct.

A Clearer Algorithm

Let us augment your pseudocode with a write-only queue Q to make it clear that the algorithm tries to reproduce the given permutation P. Since the queue is never read, it does not change the semantic of the algorithm in the question.

Initialize an empty queue Q and an empty stack S
Let In be input that produces 1, 2, ..., n.
Treat sequence P as a queue
While In is not empty:
Move the next number from In (1 then 2 then 3,...) onto S
While S is not empty and the top of S is the front of P:
Move the top of S to Q
Pop P

if S is empty
return True    # Q is the same as the original P
else
return False


The Loop Invariant.

Given P, the algorithm runs a sequence of moving actions of one of two types:

• move a number from In to S
• move a number from S to Q and pop P as well (only when the top of the S is the same as the front of P)

Here is the invariant of the whole algorithm: the algorithm always take the only possible moving action so that in the end Q might be the same as the original (input) P.

Proof: Before any moving action, the algorithm may find S and P in one of the following two states.

• S is not empty and the top of S is the same as the front of P. Let the number at the top of S (and the front of P) be s.

Suppose the algorithm moves another number i from In to S.

• Since S is a stack, i will be moved into Q before s if both of them will ever be moved to Q. Once i and s are in Q, no later actions can change the order of them in Q, since Q is a queue. So in the end, i will sit earlier than s in Q.
• On the other hand, i will only be moved into Q at the point of time t later when both the top of the stack is i and the front of P also becomes i. Since P is a queue and the front of P is s now, i must sit later than s now. In other words, i sits later than s in the original P.

The inconsistent order of i and s in Q and in the original P means this moving action from In to S cannot be successful. Hence, the only action for the algorithm to take so that in the end Q might be the same as the original P possibly is moving the number at S to Q and popping P.

• Either S is empty or the top of S is not the same as the front of P.
In this case, the only possible action for the algorithm to take is moving a number from In to S.

• Here is a proper loop invariant for the algorithm in the question. Before the start the every iteration of the while loop, the algorithm has taken the only sequence of actions possible such that, in the end, all elements that are popped from S without pushed back in the order of time being popped form the same sequence as the original input P. Apr 25 at 18:47
• Thanks alot for the detailed proof! I have noticed you never used that the input is 1,2,3,…,n ordered, if the input was randomly and not sorted would your proof still work? Apr 27 at 1:36
• Nice observation. Yes, I also noticed that when I posted the answer. I was, in fact, planning to write Let In be input that produces n distinct elements in a fixed order. If you look closely, your algorithm, as well as the one in my answer, does not depend on whether the input is ordered. Apr 27 at 1:44
• The point is in a fixed order, which ensures that the algorithm will succeed if P is stack permutable, since all the algorithm needs to do is to replay how P was obtained. (Note that moving a number from In directly to output queue can be simulated by moving it to the stack followed immediately by moving it to the output queue.) Apr 27 at 1:49
• For myself, here is a reference, stack-sortable permutations. May 2 at 21:17