namespace Freya.DataStructures.Stacks;
using System;
public

    Stack = sealed class[X]
    public
        constructor(Capacity: Integer);
        constructor: Self(128);

        iterator Stack: X;

        property IsEmpty: Boolean => Count = 0;

        property Top: X => Items[Count - 1];
            requires not IsEmpty;

        method Pop;
            requires not IsEmpty raise "Cannot call Pop on an empty stack"; 
        method Push(Value: X);
            ensures not IsEmpty, Top.Equals(Value);
    end;

implementation for Stack[X] is

    Items: Array[X];
    Count: Integer;

    constructor(Capacity: Integer);
    begin
        Items := new Array[X](Capacity);
    end;

    iterator Stack: X;
    begin
        for I := Count – 1 downto 0
            yield Items[I];
    end;

    method Pop;
    begin
        Count--;
    end;

    method Push(Value: X);
    begin
        Items[Count] := Value;
        Count++;
    ensures
        Count = old Count + 1;
    end;

end.