my homework (reply)

29-08-12

(them)

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.

Please add a directory where I indicated, to put all your code there. It will be much easier to work together, and we can remove the code afterwards if we feel this is not useful to leave it in the repository. Also, could you add there a file with Johannes instructions/questions, and your answers? This way, we can reply by updating this file, and have it evolve as you make progress.

a)
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.

4)
At first it yields run-time error
raised CONSTRAINT_ERROR : stacks.adb:47 index check failed

correct, this is the expected behavior when you try to Pop from an empty stack.

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.

That's precisely what we want to avoid. We want Pop to be called only in a context where the stack is not empty, which you can express by adding a precondition to Pop (see point (5) in instructions).

5)
it yields run-time error
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from
stacks.ads:26

correct, this is now better, you get a precondition failure when the context to call Pop is not adequate.

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

so please remove the special defensive code that you have added to Pop.

6)
I wrote another precondition for the push procedure, but I have doubts
on this point.

If you're talking of
  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

don't go into that. That's not useful for this exercise.

Right know I have just 2 tests but I'm not sure if you refer to these
kind of tests

You should have a test where you call Push on a full stack, so that it raises an exception, that you can catch in an exception block:

  begin
     Push (S, 1);
     Put_Line ("Error: Push on full stack does not raise exception");
  exception
     when Assert_Failure =>
        Put_Line ("Ok: Push on full raises exception");
  end;

8)
I don't know how to use Peek on the Pop precondition

Johannes said to use Peek in the postcondition of Push, not the precondition of Pop.

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

You can write the following postcondition of Pop:

  function Pop (S : in out Stack) return Integer with
    Post => Pop'Result = Peek (S'Old);

10)
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/

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.

12)
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

no. You can simply have a stack be a record holding a pointer to the underlying array. When the array is full, you can then reallocate a bigger one and copy all the values, then change the value of the internal pointer component.

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

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.