Artifact f675ac96a0ab25f8f25fe7ddb931494b42105f91:

Attachment "2017_09_xx_stack_by_Tucker_Taft.psl" to wiki page [Local Copies of ParaSail Deliverables] added by martin_vahi on 2017-09-29 02:21:18.

---

interface Stack
  <Component is Assignable<>; 
   Size_Type is Integer<>> is
    
    func Max_Stack_Size(S : Stack) -> Size_Type
      {Max_Stack_Size > 0};
    
    func Count(S : Stack) -> Size_Type 
      {Count <= Max_Stack_Size(S)};
    
    func Create(Max : Size_Type {Max > 0}) -> Stack 
      {Max_Stack_Size(Create) == Max; Count(Create) == 0};
    
    func Is_Empty(S : Stack) -> Boolean
      {Is_Empty == (Count(S) == 0)};
    
    func Is_Full(S : Stack) -> Boolean
      {Is_Full == (Count(S) == Max_Stack_Size(S))};
      
    func Push
      (var S : Stack {not Is_Full(S)}; 
       X : Component)
      {Count(S') == Count(S) + 1; not Is_Empty(S')};
      
    func Top(ref S : Stack) {not Is_Empty(S)} 
      -> ref Component;
    
    func Pop(var S : Stack {not Is_Empty(S)})
      -> (Component {Count(S') == Count(S) - 1; not Is_Full(S')});
    
      
end interface Stack;


class Stack <Component is Assignable<>; Size_Type is Integer<>> is
    const Max_Len : Size_Type;
    var Cur_Len : Size_Type {Cur_Len in 0..Max_Len};
    type Index_Type is Size_Type {Index_Type in 1..Max_Len};
    var Data : Array<optional Component, Indexed_By => Index_Type>;    
  exports
    {for all I in 1..Cur_Len => Data[I] not null}   // invariant for Top()

    func Max_Stack_Size(S : Stack) -> Size_Type
      {Max_Stack_Size > 0} is
	return S.Max_Len;
    end func Max_Stack_Size;
    
    func Is_Empty(S : Stack) -> Boolean
      {Is_Empty == (Count(S) == 0)} is
	return S.Cur_Len == 0;
    end func Is_Empty;
    
    func Is_Full(S : Stack) -> Boolean
      {Is_Full == (Count(S) == Max_Stack_Size(S))} is
	return S.Cur_Len == S.Max_Len;
    end func Is_Full;
      
    func Count(S : Stack) -> Size_Type is
      return S.Cur_Len;
    end func Count; 

    func Create(Max : Size_Type {Max > 0}) -> Stack
      {Max_Stack_Size(Create) == Max and Count(Create) == 0} is
      return (Max_Len => Max, Cur_Len => 0, Data => Create(1..Max, null));
    end func Create;

    func Push(var S : Stack {not Is_Full(S)}; X : Component)
      {Count(S') == Count(S) + 1} is
      S.Cur_Len += 1;      // requires not Is_Full(S) precondition
      S.Data[S.Cur_Len] := X;   // preserves invariant (see above)
    end func Push;
      
    func Top(ref S : Stack {not Is_Empty(S)}) -> ref Component is
      return S.Data[S.Cur_Len]; // requires not Is_Empty and invariant (above)
    end func Top;                

    func Pop(var S : Stack {not Is_Empty(S)}) -> Result : Component 
      {Count(S') == Count(S) - 1; not Is_Full(S')} is
        Result := Top(S);
	S.Cur_Len -= 1;
    end func Pop;
      
end class Stack;

func Test_Stack() is
    var Stk : Stack<Univ_Integer, Integer> := Create(5);

    Println("Pushing 1..5");
    Stk.Push(1);
    Stk.Push(2);
    Stk.Push(3);
    Stk.Push(4);
    Stk.Push(5);

    Println("Pop = " | Stk.Pop());
    Println("Pop = " | Stk.Pop());
    Println("Pushing 6");
    Stk.Push(6);
    Println("Pop = " | Stk.Pop());
    Println("Pop = " | Stk.Pop());
    Println("Pop = " | Stk.Pop());
    Println("Pop = " | Stk.Pop());

    // Println("About to underrun the stack");

    // Println("Pop = " | Stk.Pop());

end func Test_Stack;