pragma SPARK_Mode (On); with Stacks; function Main return Integer is package Integer_Stacks is new Stacks(Integer,0); use Integer_Stacks; S: Stack; begin Empty(S); Push(S,2); --Push(S,3); Pop(S); --if Size(S) > 0 then return Top(S); --else -- return 0; --end if; end Main;