my homework

26-08-12
(I)

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.

 

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

4)

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.

5)

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

6) 

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

8)

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

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

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

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: 

--test push

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

To compile:

gnatmake -P test.gpr

To run:

./main