However I'm back, I have not finished yet my homework but I hope I can finish tomorrow.
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
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
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from stacks.ads:26
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.
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
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 proofs.
Maybe exist a way to define vars just for pre/post scope.
--I wrote this at first, now I'm using S'old
when I compile code I get these warnings:
stacks.ads:35:27: warning: call to "Push" may occur before body is seen
stacks.ads:35:27: warning: Program_Error may be raised at run time
stacks.ads:35:27: warning: called at stacks.adb:44
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 well
I remember that on the "lighter introduction to hi-lite"
exists tests on the specification
Test_1 => (if X = 10 and Y < 9_990 then Add'Result = X + Y),
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
Right know my test are just these two:
-- For N in 1 .. Max_Size +1 loop
-- Push (S, N);
-- end loop;
-- test pop
-- X := Pop (S);
I changed the first when I create a stack of a different size.
all pre/post continue hold.
gnatmake -P test.gpr