However I'm back, I have not finished yet my homework but I hope I can
I found this observations:
I wrote code but I don't know if I should submit in git cause this is
not really part of hi-lite, so I attach in this mail.
with the "lighter introduction to hi-lite" I observed that I need /gnat
pro/ in order to use /codePeer/
maybe I won't need it but I'd say it
No, you don't need CodePeer.
At first it yields run-time error
raised CONSTRAINT_ERROR : stacks.adb:47 index check failed
then I add an "if not empty validation"
and now pop returns -2 (a constant Error_Value) when it pop an element
from an empty stack list.
it yields run-time error
RE : failed precondition from
Is better cause this is an assertion failure and not an error
This assertion is defined on the specification.
Is better cause we're giving more util information to the compiler.
And we have not to write post condition on each caller code
I wrote another precondition for the push procedure, but I have doubts
on this point.
Pre => not Is_Full (S)
then, that's the correct precondition that we expected. I see there is code commented out where you try to call Peek. I don't think that's useful here.
I saw that gnat gpl do not include GNATcoverage
I'm reading how to use gcov but still don't understand
Right know I have just 2 tests but I'm not sure if you refer to these
kind of tests
Push (S, 1);
Put_Line ("Error: Push on full stack does not raise exception");
when Assert_Failure =>
Put_Line ("Ok: Push on full raises exception");
I don't know how to use Peek on the Pop precondition
I think to save the Peeked value on the pre condition in a variable
and in the post condition compare the poped value with the previous peeked.
but I'm not sure if I should define variables used just for this kind of
Maybe exist a way to define vars just for pre/post scope.
--I wrote this at first, now I'm using S'old
function Pop (S : in out Stack) return Integer with
Post => Pop'Result = Peek (S'Old);
10)/stacks.ads:35:27: warning: call to "Push" may occur before body is seen/
when I compile code I get these warnings:
/stacks.ads:35:27: warning: Program_Error may be raised at run time/
/stacks.ads:35:27: warning: called at stacks.adb:44/
You are calling the Push recursively in its postcondition, which is not a good idea: it leads to infinite recursion. Hence the message of the compiler. Notice that Johannes asked you to call in the postcondition of the *procedure* Push a *function* also called Push that he tells you about in point (9) of the instructions.
I'm not sure what is the goal of this point
now I'm reading the chapter 10 - Access Types
I suppose that you refer to use a list instead than array
My test are not really invasive I think probably I'm not doing wellTest_1 => (*if* X = 10*and* Y < 9_990*then* Add'Result = X + Y),
I remember that on the "lighter introduction to hi-lite"
exists tests on the specification
Test_2 => (*if* X = 11*and* Y = 9_990*then* Add'Result = 10_000);
I'm almost sure that you didn't refer of above kind of test cause you
said on Main.adb
Yes, just use tests like Johannes started in main.adb
I suggest you first add the code and a file for instructions/answers to the git repository, before we continue by email.