tag:blogger.com,1999:blog-56178379813149801652024-03-07T20:16:11.108-08:00ESA SoCiS 2012 hi-litetlakatziEuroñerohttp://www.blogger.com/profile/11597687088698041136noreply@blogger.comBlogger10125tag:blogger.com,1999:blog-5617837981314980165.post-89887965594323491662012-09-14T14:13:00.005-07:002012-09-14T14:13:57.147-07:00warm-up exercise refactoring<h3>
10-09-12<br />(them)</h3>
<br />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">Could you give us a short assessment of where you are in the introductory example that we gave you as a warm-up exercise? In order for you to spend some time on the real container library, it would be good to complete this exercise this week if possible.</span><br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" /><br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" /><span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">I see you committed the exercise code+text in hi-lite/libs/containers/ada/</span><u style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;"></u><span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">in</span><wbr style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;"></wbr><span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">tro, thanks. Could you create a different version of Stacks for each extension? So the original Stacks is the simplest one, and then you can have Unbounded_Stacks and Indefinite_Stacks, etc. That will help reviewing your code.</span><br />
<br />
<h3>
14-09-12<br />(I)</h3>
<div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
I already this structure to the sources:</div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<i><br /></i></div>
<blockquote style="background-color: white; border: none; color: #222222; font-family: arial, sans-serif; font-size: 13px; margin: 0px 0px 0px 40px; padding: 0px;">
<div>
<i>indefinite_stacks</i></div>
<div>
<i>stacks</i></div>
<div>
<i>unbounded_integer_stacks</i></div>
<div>
<i>unbounded_stacks</i></div>
</blockquote>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<i><br /></i></div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
Now I'm using one main for each test:</div>
<blockquote style="background-color: white; border: none; color: #222222; font-family: arial, sans-serif; font-size: 13px; margin: 0px 0px 0px 40px; padding: 0px;">
<div>
<i>main_indefinite_stacks.adb</i></div>
<div>
<i>main_stacks.adb</i></div>
<div>
<i>main_unbounded_integer_stacks.<wbr></wbr>adb</i></div>
<div>
<i>main_unbounded_stacks.adb</i></div>
</blockquote>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<br /></div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">but I don't know if you refer to this kind of organization</span><div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
or maybe you refer a hierarchical one<br />maybe in the simplest stacks</div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
I can define base operations like</div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<div>
<br /></div>
<div>
function Is_Empty</div>
<div>
function Is_Full </div>
<div>
<br /></div>
<div>
and then on the others stacks make extends the basic operation.</div>
<div>
also maybe I can just code one larger <i>main</i> for testing</div>
<div>
<div>
<i>#main_indefinite_stacks </i>right now is just a copy of <i>unbounded_stacks</i></div>
<div>
#and <i>main.adb </i>is the old one that currently I'm not using anymore<br /></div>
</div>
<div>
<br /></div>
<h3>
14-09-12<br />(them)</h3>
<div>
This organization of code is fine.<div class="im" style="color: #500050;">
<br /><br /><blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
maybe in the simplest stacks<br />I can define base operations like<br /><br /> function Is_Empty<br /> function Is_Full<br /><br />and then on the others stacks make extends the basic operation.</blockquote>
</div>
The code is not yet clean. Could you restart from stack.ads/stack.adb and remove all unneeded operations? Just stick to the API that Johannes indicated (see INTRO.txt), which is sufficient to see and discuss issues. Remember this is just an exercise that should allow us to communicate, so the simpler the better.<br /><br /><blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
also maybe I can just code one larger /main/ for testing<br />/#main_indefinite_stacks /right now is just a copy of /unbounded_stacks/<br />#and /main.adb /is the old one that currently I'm not using anymore</blockquote>
<br />Please keep separate /main/ for each stack. That's easier to follow.</div>
</div>
</div>
tlakatziEuroñerohttp://www.blogger.com/profile/11597687088698041136noreply@blogger.com0tag:blogger.com,1999:blog-5617837981314980165.post-869898923303074082012-09-14T14:04:00.000-07:002012-09-14T14:06:38.183-07:00code style warnings<h3>
3-09-12</h3>
<h3>
(I)</h3>
<br />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">a)</span><br />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">I think that autofix option is just available for gnat pro.</span><br />
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
Do you have a "coding standard file" already generated?<br />
Theoretically I can use it to "check coding standard" option<br />
<br />
Anyway I already fixed my sources, </div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
also if when I added the "-gnatyg" flag on my test.gpr gps don't show any (style) messages</div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<br /></div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<br /></div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
But now I have a copyright issue, it yields:</div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<br /></div>
<blockquote style="background-color: white; border: none; color: #222222; font-family: arial, sans-serif; font-size: 13px; margin: 0px 0px 0px 40px; padding: 0px;">
<div>
<i>[panzon@baleada intro]$ git push</i></div>
<div>
<i>Counting objects: 17, done.</i></div>
<div>
<i>Compressing objects: 100% (12/12), done.</i></div>
<div>
<i>Writing objects: 100% (13/13), 193.76 KiB, done.</i></div>
<div>
<i>Total 13 (delta 3), reused 0 (delta 0)</i></div>
<div>
<i>remote: main.adb:70:10: Copyright notice missing, must occur before line 24</i></div>
<div>
<i>remote: Style check failed for trunk/hi-lite/libs/containers/<wbr></wbr>ada/intro/src/main.adb</i></div>
<div>
<i>remote: error: hook declined to update refs/heads/master</i></div>
<div>
<div>
<i>To git+ssh://<a href="http://panzon@scm.forge.open-do.org//scmrepos/git/hi-lite/hi-lite.git" style="color: #1155cc;" target="_blank">panzon@scm.forge.<wbr></wbr>open-do.org//scmrepos/git/hi-<wbr></wbr>lite/hi-lite.git</a></i></div>
</div>
<div>
<i> ! [remote rejected] master -> master (hook declined)</i></div>
<div>
<i>error: failed to push some refs to 'git+ssh://<a href="http://panzon@scm.forge.open-do.org//scmrepos/git/hi-lite/hi-lite.git" style="color: #1155cc;" target="_blank">panzon@scm.forge.<wbr></wbr>open-do.org//scmrepos/git/hi-<wbr></wbr>lite/hi-lite.git</a>'</i></div>
</blockquote>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<br /></div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<br /></div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
I took a look and I saw that hi-lite have different copyright headers</div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<br /></div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
b)</div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
Do I should use this one?</div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<br /></div>
<blockquote style="background-color: white; border: none; color: #222222; font-family: arial, sans-serif; font-size: 13px; margin: 0px 0px 0px 40px; padding: 0px;">
<div>
------------------------------<wbr></wbr>------------------------------<wbr></wbr>------------------</div>
<div>
-- --</div>
<div>
-- INTRO COMPONENTS --</div>
<div>
-- --</div>
<div>
-- W H Y - G E N - N A M E _ G E N --</div>
<div>
-- --</div>
<div>
-- B o d y --</div>
<div>
-- --</div>
<div>
-- Copyright (C) 2010-2012, AdaCore --</div>
<div>
-- --</div>
<div>
-- intro is free software; you can redistribute it and/or modify it --</div>
<div>
-- under terms of the GNU General Public License as published by the Free --</div>
<div>
-- Software Foundation; either version 3, or (at your option) any later --</div>
<div>
-- version. gnat2why is distributed in the hope that it will be useful, --</div>
<div>
-- but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHAN- --</div>
<div>
-- TABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public --</div>
<div>
-- License for more details. You should have received a copy of the GNU --</div>
<div>
-- General Public License distributed with gnat2why; see file COPYING3. --</div>
<div>
-- If not, go to <a href="http://www.gnu.org/licenses" style="color: #1155cc;" target="_blank">http://www.gnu.org/licenses</a> for a complete copy of the --</div>
<div>
-- license. --</div>
<div>
-- --</div>
<div>
-- intro is maintained by AdaCore (<a href="http://www.adacore.com/" style="color: #1155cc;" target="_blank">http://www.adacore.com</a>) --</div>
<div>
-- --</div>
<div>
------------------------------<wbr></wbr>------------------------------<wbr></wbr>------------------</div>
</blockquote>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<br /></div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<br /></div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
<div>
I just substitute intro instead WHY</div>
<div>
or maybe you already have some script that generate this header.</div>
<div>
<br /></div>
<h3>
3-09-12<br />(them)</h3>
<div>
<div class="im" style="color: #500050;">
On 09/03/2012 04:28 PM, Ricardo Aguirre wrote:<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
a)<br />
I think that autofix option is just available for gnat pro.</blockquote>
</div>
No, when you compile inside GPS with the option -gnatyg, and if you get style warnings like the ones you sent us, then you should have a small icon on the left side of the warning *and* the same icon on the left side of the line with a warning that allows you to autofix the problem by clicking on the icon.<br />
<div class="im" style="color: #500050;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
Do you have a "coding standard file" already generated?</blockquote>
</div>
Didn't you see the attachment in my previous email? This is the coding standard we use at AdaCore.<br />
<div class="im" style="color: #500050;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
Theoretically I can use it to "check coding standard" option</blockquote>
</div>
Do you mean an input file to gnatcheck?<br />
<div class="im" style="color: #500050;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
Anyway I already fixed my sources,</blockquote>
</div>
ok, good.<br />
<div class="im" style="color: #500050;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
also if when I added the "-gnatyg" flag on my test.gpr gps don't show<br />
any (style) messages</blockquote>
</div>
good, keep it then in your project file.<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
<div class="im" style="color: #500050;">
But now I have a copyright issue, it yields:</div>
/[panzon@baleada intro]$ git push/<br />
/Counting objects: 17, done./<br />
/Compressing objects: 100% (12/12), done./<br />
/Writing objects: 100% (13/13), 193.76 KiB, done./<br />
/Total 13 (delta 3), reused 0 (delta 0)/<br />
/remote: main.adb:70:10: Copyright notice missing, must occur before<br />
line 24/<br />
/remote: Style check failed for<br />
trunk/hi-lite/libs/containers/<u></u><wbr></wbr>ada/intro/src/main.adb/<br />
/remote: error: hook declined to update refs/heads/master/<br />
/To<br />
git+ssh://<a href="http://panzon@scm.forge.open-do.org//scmrepos/git/hi-lite/hi-lite.git" style="color: #1155cc;" target="_blank">panzon@scm.forge.<u></u>ope<wbr></wbr>n-do.org//scmrepos/git/hi-<u></u>lite<wbr></wbr>/hi-lite.git</a><br />
<<a href="http://panzon@scm.forge.open-do.org//scmrepos/git/hi-lite/hi-lite.git" style="color: #1155cc;" target="_blank">http://panzon@scm.forge.open-<u></u><wbr></wbr>do.org//scmrepos/git/hi-lite/<u></u>h<wbr></wbr>i-lite.git</a>>/<br />
/ ! [remote rejected] master -> master (hook declined)/<br />
/error: failed to push some refs to<br />
'git+ssh://<a href="http://panzon@scm.forge.open-do.org//scmrepos/git/hi-lite/hi-lite.git" style="color: #1155cc;" target="_blank">panzon@scm.forge.<u></u>op<wbr></wbr>en-do.org//scmrepos/git/hi-<u></u>lit<wbr></wbr>e/hi-lite.git</a><br />
<<a href="http://panzon@scm.forge.open-do.org//scmrepos/git/hi-lite/hi-lite.git" style="color: #1155cc;" target="_blank">http://panzon@scm.forge.open-<u></u><wbr></wbr>do.org//scmrepos/git/hi-lite/<u></u>h<wbr></wbr>i-lite.git</a>>'/<br />
<div class="im" style="color: #500050;">
<br />
<br />
I took a look and I saw that hi-lite have different copyright headers</div>
</blockquote>
<br />
Ah yes, you should not bother about copyright at this stage.<br />
I have committed a change to .gitattributes so that you don't have this problem anymore (you can see my change after you update your repository). Retry committing now (after doing a "git pull --rebase" and checking you have no conflicts of course).<br />
<br />
<h3>
14-09-12<br />(them)</h3>
</div>
<div>
<div class="im" style="color: #500050;">
On Fri 14 Sep 2012 01:34:57 AM CEST, Ricardo Aguirre wrote:<br /><blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
>>Do you mean an input file to gnatcheck?<br /><br />Maybe yes, I'm not pretty sure<br /><br />When I click the right button on the editor<br />it appears "check coding standard" option<br />if I click it<br />then it appears this message (attached image).<br />I meant that file.</blockquote>
</div>
You are trying to use GNATcheck. This is not what I meant by using our coding style. Most rules in our coding style have to do with spacing/indentation/naming of entities and do not require GNATcheck. They are simple enough that you can follow them easily while developing, if you take the time to read the coding style pdf that I sent you.</div>
<div>
<br /></div>
<div>
BTW, I just tried to compile your code, and I get various warnings related to style problems, that should be corrected:<br /><br />$ gnatmake -P test<br />unbounded_stacks.ads:40:36: (style) space required<br />main_stacks.adb:33:03: (style) incorrect layout<br />main_stacks.adb:41:03: (style) incorrect layout<br />stacks.ads:11:80: (style) this line is too long<br />stacks.ads:48:04: (style) horizontal tab not allowed<br />stacks.ads:54:80: (style) this line is too long</div>
</div>
tlakatziEuroñerohttp://www.blogger.com/profile/11597687088698041136noreply@blogger.com0tag:blogger.com,1999:blog-5617837981314980165.post-8524535901980763572012-09-14T13:57:00.000-07:002012-09-14T13:57:29.045-07:00hook problems<h3>
3-09-12<br />(them)</h3>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;"> it is important that you concentrate now on being able to commit your work in git. I give you below the reason for the error you got so far, that should be easy to correct.</span><br />
<div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br /><br />On 09/02/2012 10:52 PM, Ricardo Aguirre wrote:</div>
<blockquote class="gmail_quote" style="background-color: white; border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; color: #222222; font-family: arial, sans-serif; font-size: 13px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
<div class="im" style="color: #500050;">
I already solved the 13)<br /><br />My error was incredible stupid!<br /><br />Now I have problems with git<br />last week I setup my global git configuration on my pc, I used this email:</div>
<a href="mailto:panzon@scm.forge.open-do.org" style="color: #1155cc;" target="_blank">panzon@scm.forge.open-do.org</a> <mailto:<a href="mailto:panzon@scm.forge.open-do.org" style="color: #1155cc;" target="_blank">panzon@scm.forge.open-<u></u><wbr></wbr>do.org</a>><div class="im" style="color: #500050;">
<br />now I'm getting this errors:<br /><a href="http://pastebin.com/ST85qZnj" style="color: #1155cc;" target="_blank">http://pastebin.com/ST85qZnj</a></div>
</blockquote>
<br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" /><span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">Ok, you're having hook problems. We have a hook that checks that the code you commit complies to GNAT style checks before allowing you to commit them. You can check these rules on your computer by compiling with switch -gnatyg. Many of these rules are so simple (indentation, spacing) that you can correct them in GPS by clicking on a small icon on the side that says "autofix". BTW, you can set up GPS so that it does the indentation automatically for you. I am joining the Ada Coding Style that we use at AdaCore.</span><div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br /><br /><blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
12)<br />at first it yields<br />raised SYSTEM.ASSERTIONS.ASSERT_<u></u>FAILU<wbr></wbr>RE : failed precondition from stacks.ads:39<br /><br />Then I removed the old push precondition (not Is_Full(S))<br />now is running</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">I guess it's ok, but here it would really help that you commit the questions and your current answers in a file that I can inspect.</span><div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br /><br /><blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
13)<br />I'm stocked with generics, I already read many chapters of ada book, but I'm doing something wrong, I hope I'll solve it during this weekend.<br />Now I see that stack example is really classic, and book talk about it in many chapters, actually I feel little embarrassed cause I'm having problems with really basic stuffs. However I'm working in.</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">Don't worry, the goal of this exercise is precisely to help you figure out the problems in a simplified setting, so that we can help you more easily before you attack the real library.</span><div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br /><br /><blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
14)<br />To solve this point I have to ideas:<br />a) do not use anymore the array instead use a list, like the Cell example</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">Yes, that's what we had in mind.</span><div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br /><br /><blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
b) Use a type base, and then all objects inserted on the array should be<br />subtype of this base type. Doing an analogy with java that each object<br />extends implicitly from Object Class.</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">We have the same notion of derivation in Ada: an object of type T'Class can be dynamically of any type derived from T. Except you cannot put T'Class objects in an array, because they do not have a fixed size. So the solution is really to use pointers.</span><br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" /><br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" /><blockquote class="gmail_quote" style="background-color: white; border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; color: #222222; font-family: arial, sans-serif; font-size: 13px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
<div class="im" style="color: #500050;">
8)<br />When I tried to use your suggested postcondition<br />it yields:</div>
/raised SYSTEM.ASSERTIONS.ASSERT_<u></u>FAILU<wbr></wbr>RE : failed postcondition from<br />stacks.ads:49 instantiated at main.adb:5/<div class="im" style="color: #500050;">
<br /><br />I'm not pretty sure about the reason of this message.</div>
</blockquote>
<br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" /><span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">Either your postcondition is wrong, or your implementation of Push is wrong. At least they do not match. Try inspecting values by debugging or printing to see which one it is.</span>tlakatziEuroñerohttp://www.blogger.com/profile/11597687088698041136noreply@blogger.com0tag:blogger.com,1999:blog-5617837981314980165.post-6408664994441966652012-09-14T13:17:00.004-07:002012-09-14T13:19:33.050-07:00My homework doubts<h3>
1-09-12<br />(I)</h3>
<br />
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
Since yesterday I tried to push some changes and at first it yields error on web (when I tried to verify, if my changes was really commited)</div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
this morning also the console</div>
<blockquote style="background-color: white; border: none; color: #222222; font-family: arial, sans-serif; font-size: 13px; margin: 0px 0px 0px 40px; padding: 0px;">
<div>
<i>[panzon@baleada intro]$ git pull</i></div>
<div>
<i>ssh: connect to host <a href="http://scm.forge.open-do.org/" style="color: #1155cc;" target="_blank">scm.forge.open-do.org</a> port 22: Connection timed out</i></div>
<div>
<i>fatal: The remote end hung up unexpectedly</i></div>
</blockquote>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
</div>
<div style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">
12)<br />
at first it yields<br />
<div>
raised SYSTEM.ASSERTIONS.ASSERT_<wbr></wbr>FAILURE : failed precondition from stacks.ads:39<br />
<div>
<br />
Then I removed the old push precondition (not Is_Full(S))</div>
<div>
now is running<br />
<br />
13) </div>
<div>
<div>
I'm stocked with generics, I already read many chapters of ada book, but I'm doing something wrong, I hope I'll solve it during this weekend.</div>
<div>
Now I see that stack example is really classic, and book talk about it in many chapters, actually I feel little embarrassed cause I'm having problems with really basic stuffs. However I'm working in.<br />
<br />
<h3>
2-09-12<br />(I)</h3>
<br />
I already solved the 13)<br />
<div>
<br />My error was incredible stupid!<br /><br />Now I have problems with git<br />last week I setup my global git configuration on my pc, I used this email:<br /><a href="mailto:panzon@scm.forge.open-do.org" style="color: #1155cc;" target="_blank">panzon@scm.forge.open-do.org</a></div>
<div>
now I'm getting this errors:</div>
<div>
<a href="http://pastebin.com/ST85qZnj" style="color: #1155cc;" target="_blank">http://pastebin.com/ST85qZnj</a><br /></div>
<div>
14)<br clear="all" />To solve this point I have to ideas:</div>
<div>
a) do not use anymore the array instead use a list, like the Cell example<br />b) Use a type base, and then all objects inserted on the array should be subtype of this base type. Doing an analogy with java that each object extends implicitly from Object Class.</div>
<div>
<br />What do you think?</div>
<div>
<br /></div>
<div>
8)</div>
<div>
When I tried to use your suggested postcondition </div>
<div>
it yields:</div>
<div>
<i>raised SYSTEM.ASSERTIONS.ASSERT_<wbr></wbr>FAILURE : failed postcondition from stacks.ads:49 instantiated at main.adb:5</i></div>
<div>
<i><br /></i></div>
</div>
</div>
</div>
</div>
tlakatziEuroñerohttp://www.blogger.com/profile/11597687088698041136noreply@blogger.com0tag:blogger.com,1999:blog-5617837981314980165.post-51780087009300462292012-09-14T13:16:00.001-07:002012-09-14T13:58:09.934-07:00my homework (reply)<h3>
29-08-12</h3>
<h3>
(them)</h3>
<div>
<br />
<div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
However I'm back, I have not finished yet my homework but I hope I can<br />
finish tomorrow.<br />
I found this observations:<br />
I wrote code but I don't know if I should submit in git cause this is<br />
not really part of hi-lite, so I attach in this mail.</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">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.</span><br />
<br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" />
<blockquote class="gmail_quote" style="background-color: white; border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; color: #222222; font-family: arial, sans-serif; font-size: 13px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
a)<br />
with the "lighter introduction to hi-lite" I observed that I need /gnat<br />
pro/ in order to use /codePeer/<br />
<div class="im" style="color: #500050;">
<br />
maybe I won't need it but I'd say it</div>
</blockquote>
<br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">No, you don't need CodePeer.</span><br />
<div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
4)<br />
At first it yields run-time error<br />
raised CONSTRAINT_ERROR : stacks.adb:47 index check failed</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">correct, this is the expected behavior when you try to Pop from an empty stack.</span><br />
<div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
then I add an "if not empty validation"<br />
and now pop returns -2 (a constant Error_Value) when it pop an element<br />
from an empty stack list.</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">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).</span><br />
<div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
5)<br />
it yields run-time error<br />
raised SYSTEM.ASSERTIONS.ASSERT_<u></u>FAILU<wbr></wbr>RE : failed precondition from<br />
stacks.ads:26</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">correct, this is now better, you get a precondition failure when the context to call Pop is not adequate.</span><br />
<div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
Is better cause this is an assertion failure and not an error<br />
This assertion is defined on the specification.<br />
Is better cause we're giving more util information to the compiler.<br />
And we have not to write post condition on each caller code</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">so please remove the special defensive code that you have added to Pop.</span><br />
<div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
6)<br />
I wrote another precondition for the push procedure, but I have doubts<br />
on this point.</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">If you're talking of</span><br />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;"> Pre => not Is_Full (S)</span><br />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">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.</span><br />
<div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
I saw that gnat gpl do not include GNATcoverage<br />
I'm reading how to use gcov but still don't understand</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">don't go into that. That's not useful for this exercise.</span><br />
<div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
Right know I have just 2 tests but I'm not sure if you refer to these<br />
kind of tests</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">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:</span><br />
<br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;"> begin</span><br />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;"> Push (S, 1);</span><br />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;"> Put_Line ("Error: Push on full stack does not raise exception");</span><br />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;"> exception</span><br />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;"> when Assert_Failure =></span><br />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;"> Put_Line ("Ok: Push on full raises exception");</span><br />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;"> end;</span><br />
<div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
8)<br />
I don't know how to use Peek on the Pop precondition</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">Johannes said to use Peek in the postcondition of Push, not the precondition of Pop.</span><br />
<div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
I think to save the Peeked value on the pre condition in a variable<br />
and in the post condition compare the poped value with the previous peeked.<br />
but I'm not sure if I should define variables used just for this kind of<br />
proofs.<br />
Maybe exist a way to define vars just for pre/post scope.<br />
<br />
--I wrote this at first, now I'm using S'old</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">You can write the following postcondition of Pop:</span><br />
<br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;"> function Pop (S : in out Stack) return Integer with</span><br />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;"> Post => Pop'Result = Peek (S'Old);</span><br />
<br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" />
<blockquote class="gmail_quote" style="background-color: white; border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; color: #222222; font-family: arial, sans-serif; font-size: 13px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
<div class="im" style="color: #500050;">
10)<br />
when I compile code I get these warnings:</div>
/stacks.ads:35:27: warning: call to "Push" may occur before body is seen/<br />
/stacks.ads:35:27: warning: Program_Error may be raised at run time/<br />
/stacks.ads:35:27: warning: called at stacks.adb:44/</blockquote>
<br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">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.</span><br />
<div class="im" style="background-color: white; color: #500050; font-family: arial, sans-serif; font-size: 13px;">
<br />
<br />
<blockquote class="gmail_quote" style="border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
12)<br />
I'm not sure what is the goal of this point<br />
now I'm reading the chapter 10 - Access Types<br />
I suppose that you refer to use a list instead than array</blockquote>
</div>
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">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.</span><br />
<br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" />
<blockquote class="gmail_quote" style="background-color: white; border-left-color: rgb(204, 204, 204); border-left-style: solid; border-left-width: 1px; color: #222222; font-family: arial, sans-serif; font-size: 13px; margin: 0px 0px 0px 0.8ex; padding-left: 1ex;">
<div class="im" style="color: #500050;">
My test are not really invasive I think probably I'm not doing well<br />
I remember that on the "lighter introduction to hi-lite"<br />
exists tests on the specification</div>
Test_1 => (*if* X = 10*and* Y < 9_990*then* Add'Result = X + Y),<br />
Test_2 => (*if* X = 11*and* Y = 9_990*then* Add'Result = 10_000);<br />
<div class="im" style="color: #500050;">
<br />
<br />
I'm almost sure that you didn't refer of above kind of test cause you<br />
said on Main.adb</div>
</blockquote>
<br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">Yes, just use tests like Johannes started in main.adb</span><br />
<br style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;" />
<span style="background-color: white; color: #222222; font-family: arial, sans-serif; font-size: 13px;">I suggest you first add the code and a file for instructions/answers to the git repository, before we continue by email.</span></div>
tlakatziEuroñerohttp://www.blogger.com/profile/11597687088698041136noreply@blogger.com0tag:blogger.com,1999:blog-5617837981314980165.post-8905221080712619322012-09-14T13:12:00.000-07:002012-09-14T13:12:26.884-07:00my homework<h3>
26-08-12<br />(I)</h3>
<div>
<div>
However I'm back, I have not finished yet my homework but I hope I can finish tomorrow.</div>
<div>
I found this observations:</div>
<div>
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.</div>
<div>
</div>
<div>
a)</div>
<div>
with the "lighter introduction to hi-lite" I observed that I need gnat pro in order to use codePeer</div>
<div>
maybe I won't need it but I'd say it</div>
<div>
<br /></div>
<div>
4)</div>
<div>
At first it yields run-time error</div>
<div>
raised CONSTRAINT_ERROR : stacks.adb:47 index check failed</div>
<div>
then I add an "if not empty validation"</div>
<div>
and now pop returns -2 (a constant Error_Value) when it pop an element from an empty stack list.</div>
<div>
<br /></div>
<div>
5)</div>
<div>
it yields run-time error</div>
<div>
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from stacks.ads:26</div>
<div>
<br /></div>
<div>
Is better cause this is an assertion failure and not an error</div>
<div>
This assertion is defined on the specification. </div>
<div>
Is better cause we're giving more util information to the compiler.</div>
<div>
And we have not to write post condition on each caller code</div>
<div>
<br /></div>
<div>
6) </div>
<div>
I wrote another precondition for the push procedure, but I have doubts on this point.</div>
<div>
<br /></div>
<div>
I saw that gnat gpl do not include GNATcoverage</div>
<div>
I'm reading how to use gcov but still don't understand</div>
<div>
<br /></div>
<div>
Right know I have just 2 tests but I'm not sure if you refer to these kind of tests</div>
<div>
<br /></div>
<div>
8)</div>
<div>
I don't know how to use Peek on the Pop precondition</div>
<div>
I think to save the Peeked value on the pre condition in a variable</div>
<div>
and in the post condition compare the poped value with the previous peeked.</div>
<div>
but I'm not sure if I should define variables used just for this kind of proofs.</div>
<div>
Maybe exist a way to define vars just for pre/post scope. </div>
<div>
<br /></div>
<div>
--I wrote this at first, now I'm using S'old</div>
<div>
<br /></div>
<div>
10)</div>
<div>
when I compile code I get these warnings:</div>
<div>
stacks.ads:35:27: warning: call to "Push" may occur before body is seen</div>
<div>
stacks.ads:35:27: warning: Program_Error may be raised at run time</div>
<div>
stacks.ads:35:27: warning: called at stacks.adb:44</div>
<div>
<br /></div>
<div>
12)</div>
<div>
I'm not sure what is the goal of this point</div>
<div>
now I'm reading the chapter 10 - Access Types</div>
<div>
I suppose that you refer to use a list instead than array</div>
<div>
<br /></div>
<div>
My test are not really invasive I think probably I'm not doing well</div>
<div>
I remember that on the "lighter introduction to hi-lite" </div>
<div>
exists tests on the specification</div>
<div>
Test_1 => (if X = 10 and Y < 9_990 then Add'Result = X + Y),</div>
<div>
Test_2 => (if X = 11 and Y = 9_990 then Add'Result = 10_000);</div>
<div>
I'm almost sure that you didn't refer of above kind of test cause you said on Main.adb</div>
<div>
Right know my test are just these two: </div>
<div>
<br /></div>
<div>
--test push</div>
<div>
-- For N in 1 .. Max_Size +1 loop</div>
<div>
-- Push (S, N);</div>
<div>
-- end loop;</div>
<div>
<br /></div>
<div>
-- test pop</div>
<div>
-- X := Pop (S);</div>
<div>
<br /></div>
<div>
I changed the first when I create a stack of a different size.</div>
<div>
all pre/post continue hold.</div>
<div>
<br /></div>
<div>
<br /></div>
<div>
To compile:</div>
<div>
gnatmake -P test.gpr</div>
<div>
<br /></div>
<div>
To run:</div>
<div>
./main</div>
</div>
tlakatziEuroñerohttp://www.blogger.com/profile/11597687088698041136noreply@blogger.com0tag:blogger.com,1999:blog-5617837981314980165.post-67074901938183523422012-09-14T13:08:00.001-07:002012-09-14T13:08:53.597-07:00get your hands dirty and write some code<h3>
9-08-12<br />(them)</h3>
<div>
<div>
So indeed it's a good time to get your hands dirty and write some code,</div>
<div>
play with the containers, Ada 2012, contracts ...</div>
<div>
<br /></div>
<div>
The "lighter introduction to hi-lite" is a good start, but it shouldn't</div>
<div>
take you too long. By the way, you can find the code in</div>
<div>
<br /></div>
<div>
testsuite/gnatprove/tests/intro</div>
<div>
<br /></div>
<div>
After that, here is a homework assignment to get you started with contracts.</div>
<div>
<br /></div>
<div>
1) Write a stack package whose spec (stacks.ads) looks a bit like that:</div>
<div>
<br /></div>
<div>
package Stacks is</div>
<div>
-- A stack package that holds integers</div>
<div>
<br /></div>
<div>
Max_Size : constant Integer := 1000;</div>
<div>
-- the maximal number of elements in the stack</div>
<div>
<br /></div>
<div>
type Content_Type is array (1 .. Max_Size) of Integer;</div>
<div>
-- the array that holds the elements</div>
<div>
<br /></div>
<div>
type Stack is record</div>
<div>
Content : Content_Type;</div>
<div>
Index : Integer;</div>
<div>
end record;</div>
<div>
<br /></div>
<div>
function Create return Stack;</div>
<div>
<br /></div>
<div>
function Is_Empty (S : Stack) return Boolean;</div>
<div>
<br /></div>
<div>
function Is_Full (S : Stack) return Boolean;</div>
<div>
<br /></div>
<div>
procedure Push (S : in out Stack; X : Integer);</div>
<div>
-- push a new element on the stack</div>
<div>
<br /></div>
<div>
procedure Pop (S : in out Stack; X : out Integer);</div>
<div>
-- remove the topmost element from the stack, and return it in X</div>
<div>
<br /></div>
<div>
function Pop (S : in out Stack) return Integer;</div>
<div>
-- same as the above procedure, but return the topmost element,</div>
<div>
-- instead of having an out parameter</div>
<div>
-- note that only in Ada 2012 functions can have in out parameters.</div>
<div>
end Stacks;</div>
<div>
<br /></div>
<div>
2) Write an implementation for this package (stacks.adb). The Stack is</div>
<div>
an array, together with an index that points to the first empty cell, or</div>
<div>
to last used cell, as you wish.</div>
<div>
<br /></div>
<div>
3) Write a main program that tests your stack implementation. It could</div>
<div>
look as follows (main.adb):</div>
<div>
<br /></div>
<div>
with Stacks; use Stacks;</div>
<div>
<br /></div>
<div>
procedure Main is</div>
<div>
S : Stack := Create;</div>
<div>
X : Integer;</div>
<div>
begin</div>
<div>
pragma Assert (Is_Empty (S));</div>
<div>
Push (S, 1);</div>
<div>
pragma Assert (not (Is_Empty (S)));</div>
<div>
Pop (S, X);</div>
<div>
pragma Assert (X = 1);</div>
<div>
pragma Assert (Is_Empty (S));</div>
<div>
Push (S, 2);</div>
<div>
Push (S, 3);</div>
<div>
Push (S, 4);</div>
<div>
X := Pop (S);</div>
<div>
pragma Assert (X = 4);</div>
<div>
X := Pop (S);</div>
<div>
pragma Assert (X = 3);</div>
<div>
X := Pop (S);</div>
<div>
pragma Assert (X = 2);</div>
<div>
pragma Assert (Is_Empty (S));</div>
<div>
end Main;</div>
<div>
<br /></div>
<div>
Obviously, when you run your program, none of the assertions should</div>
<div>
fail! Be sure to compile with option "-gnata".</div>
<div>
<br /></div>
<div>
Best is to write a project file, such as "test.gpr", with the following</div>
<div>
contents:</div>
<div>
<br /></div>
<div>
project Test is</div>
<div>
<br /></div>
<div>
for Object_Dir use "obj";</div>
<div>
for Exec_Dir use ".";</div>
<div>
for Main use ("main.adb");</div>
<div>
<br /></div>
<div>
package Compiler is</div>
<div>
for Default_Switches ("ada") use ("-gnat12", "-gnata");</div>
<div>
end Compiler;</div>
<div>
<br /></div>
<div>
end Test;</div>
<div>
<br /></div>
<div>
<br /></div>
<div>
You can now compile your project with</div>
<div>
<br /></div>
<div>
$ gnatmake -P test.gpr</div>
<div>
<br /></div>
<div>
4) What happens when you add the following line at the end of the Main</div>
<div>
procedure:</div>
<div>
<br /></div>
<div>
X := Pop (S);</div>
<div>
<br /></div>
<div>
5) You can protect yourself against what happens in (4) if you add a</div>
<div>
precondition to Pop:</div>
<div>
<br /></div>
<div>
procedure Pop (S : in out Stack; X : out Integer)</div>
<div>
with Pre => (not Is_Empty (S));</div>
<div>
<br /></div>
<div>
What happens now if you run the main program of (4)? In what way is that</div>
<div>
better than what happened in (4)?</div>
<div>
<br /></div>
<div>
6) Write more preconditions, so that any runtime error in your stacks</div>
<div>
package is impossible. Write a few tests in main.adb to check that.</div>
<div>
<br /></div>
<div>
7) Write postconditions that you know are true after executing a</div>
<div>
subprogram. For example, you know that after a "push", the stack is not</div>
<div>
empty, and after a "pop", it is not full.</div>
<div>
<br /></div>
<div>
8) Pre/ and Postconditions should never have side effects. There is a</div>
<div>
problem with that, because it means you cannot use Push and Pop in</div>
<div>
pre/post. A way to solve this is to write functions without side</div>
<div>
effects, that do something similar to push and pop, but without changing</div>
<div>
the stack. For example, you can write a function Peek that returns the</div>
<div>
topmost element of the stack without removing it. You can then write in</div>
<div>
the postcondition of push:</div>
<div>
<br /></div>
<div>
Peek (S) = X</div>
<div>
<br /></div>
<div>
to express that the topmost element is the one we just pushed.</div>
<div>
<br /></div>
<div>
Write the function Peek and use it in the pre/post.</div>
<div>
<br /></div>
<div>
9) The proposed solution in (8) solves only half of the problem, it</div>
<div>
gives an alternative to Pop, but not to Push. For Push, what we need is</div>
<div>
a *function* Push that leaves the current Stack alone and returns a new</div>
<div>
stack with the new element on top:</div>
<div>
<br /></div>
<div>
function Push (S : Stack; X : Integer) return Stack;</div>
<div>
<br /></div>
<div>
Note that "S" is an "in" parameter and is not modified. So Push must</div>
<div>
make a copy of S, modify the copy, and then return that modified copy.</div>
<div>
<br /></div>
<div>
10) Use the function of (9) in your pre/post. For example, a complete</div>
<div>
contract of the procedure Push is now the following:</div>
<div>
<br /></div>
<div>
procedure Push (S : in out Stack; X : Integer)</div>
<div>
with Pre => (not Is_Full (S)),</div>
<div>
with Post => (S = Push(S'Old, X));</div>
<div>
<br /></div>
<div>
we have used S'Old to refer to the previous value of S, ie the stack S</div>
<div>
before pushing.</div>
<div>
<br /></div>
<div>
11) With the package, one can only create stacks that all have the same</div>
<div>
fixed size. How can you change it to create stacks that have a different</div>
<div>
maximal size? You need to change the type definition, and the function</div>
<div>
Create, which now has an argument for the maximal size.</div>
<div>
Hint: use discriminant records.</div>
<div>
Change your tests and run them to see if all assertions and</div>
<div>
pre/postconditions still hold.</div>
<div>
<br /></div>
<div>
12) Write a version of stacks that can hold any number of integers. This</div>
<div>
means that at some point you need to reallocate memory. It also means</div>
<div>
that you probably need to use pointers (access).</div>
<div>
Change your tests and run them to see if all assertions and</div>
<div>
pre/postconditions still hold.</div>
<div>
<br /></div>
<div>
13) Write a version of stacks that can hold any definite object (whose</div>
<div>
size is statically known), not just Integer. Use the Ada feature of</div>
<div>
generic packages for that.</div>
<div>
Change your tests and run them to see if all assertions and</div>
<div>
pre/postconditions still hold.</div>
<div>
<br /></div>
<div>
14) Write a version of stacks that can hold any object, even objects of</div>
<div>
mixed size. You probably need to use pointers again.</div>
<div>
Change your tests and run them to see if all assertions and</div>
<div>
pre/postconditions still hold.</div>
<div>
<br /></div>
<div>
15) Feel free to write an Ada program that uses your stack, and does</div>
<div>
something useful, add pre/post to your own program ...</div>
<div>
<br /></div>
<div>
16) I forgot another aspect of the example. Make the type Stack private.</div>
<div>
Does this change anything for the implementation of the stack, and for</div>
<div>
the clients of the stack?</div>
<div>
<br /></div>
<div>
<br /></div>
<div>
<br /></div>
<div>
I'm not sure how long this may take you, this assignment is really just</div>
<div>
to get you started, feel free to abandon this whenever you think you</div>
<div>
have understood the point. You can then look at the code of the Ada 2005</div>
<div>
containers, to see how things are done "in real code". You can start</div>
<div>
thinking what kinds of pre/post you would write for the Ada 2005</div>
<div>
containers. You can also start writing functions without side effects</div>
<div>
that correspond to the procedures that modify a container, as in</div>
<div>
exercise 9 and 10.</div>
</div>
tlakatziEuroñerohttp://www.blogger.com/profile/11597687088698041136noreply@blogger.com0tag:blogger.com,1999:blog-5617837981314980165.post-11284366481617450412012-09-14T13:06:00.002-07:002012-09-14T13:06:52.852-07:00reviewing the list of source files<h3>
6-08-12<br />(I)</h3>
<div>
<div>
I reviewed the list of source files and I saw that practically the unique changed file is hi-lite/libs/containers/ada/DLL/a-cfdlli.ads </div>
<div>
the rest of file list are the same, that was distributed on the gnat gpl version. </div>
<div>
<br /></div>
<div>
Original-file-list<span class="Apple-tab-span" style="white-space: pre;"> </span>Hi-lite sources<span class="Apple-tab-span" style="white-space: pre;"> </span>Rts-native<span class="Apple-tab-span" style="white-space: pre;"> </span>Rts-sjlj</div>
<div>
a-cbdlli.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cbdlli.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cbdlli.ads</div>
<div>
a-cbhama.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cbhama.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cbhama.ads</div>
<div>
a-cbhase.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cbhase.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cbhase.ads</div>
<div>
a-cborma.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cborma.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cborma.ads</div>
<div>
a-cborse.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cborse.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cborse.ads</div>
<div>
a-cdlili.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cdlili.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cdlili.ads</div>
<div>
a-cfdlli.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/Altro/socis/hi-lite/libs/containers/ada/DLL/a-cfdlli.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cfdlli.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cfdlli.ads</div>
<div>
a-cfhama.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/Altro/socis/hi-lite/libs/containers/ada/HAMA/a-cfhama.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cfhama.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cfhama.ads</div>
<div>
a-cfhase.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/Altro/socis/hi-lite/libs/containers/ada/HASE/a-cfhase.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cfhase.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cfhase.ads</div>
<div>
a-cforma.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/Altro/socis/hi-lite/libs/containers/ada/ORMA/a-cforma.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cforma.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cforma.ads</div>
<div>
a-cforse.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/Altro/socis/hi-lite/libs/containers/ada/ORSE/a-cforse.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cforse.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cforse.ads</div>
<div>
a-cidlli.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cidlli.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cidlli.ads</div>
<div>
a-cihama.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cihama.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cihama.ads</div>
<div>
a-cihase.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cihase.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cihase.ads</div>
<div>
a-ciorma.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-ciorma.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-ciorma.ads</div>
<div>
a-ciormu.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-ciormu.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-ciormu.ads</div>
<div>
a-ciorse.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-ciorse.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-ciorse.ads</div>
<div>
a-cobove.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cobove.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cobove.ads</div>
<div>
a-cofove.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/Altro/socis/hi-lite/libs/containers/ada/VE/a-cofove.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cofove.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cofove.ads</div>
<div>
a-cohama.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cohama.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cohama.ads</div>
<div>
a-cohase.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cohase.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cohase.ads</div>
<div>
a-coinve.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-coinve.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-coinve.ads</div>
<div>
a-convec.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-convec.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-convec.ads</div>
<div>
a-coorma.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-coorma.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-coorma.ads</div>
<div>
a-coormu.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-coormu.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-coormu.ads</div>
<div>
a-coorse.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-coorse.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-coorse.ads</div>
<div>
a-crdlli.ads<span class="Apple-tab-span" style="white-space: pre;"> </span></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-crdlli.ads<span class="Apple-tab-span" style="white-space: pre;"> </span>/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-crdlli.ads</div>
<div>
<br /></div>
<div>
At first I want to ask you about nomenclature, what does DLL, HAMA, HASE, ORMA, ORSE and VE mean?</div>
<div>
Should I use the same source files? like a-cobove.ads to write new code for Replace_Element, this procedure is used in lists and Vectors</div>
<div>
if I have to define new source files</div>
<div>
Should I use the large naming style (i.e., ada-containers-bounded_vectors.ads) or short style ((i.e., a-cobove.ads)?</div>
</div>
<div>
<br /></div>
<div>
<br /></div>
tlakatziEuroñerohttp://www.blogger.com/profile/11597687088698041136noreply@blogger.com0tag:blogger.com,1999:blog-5617837981314980165.post-46779658825163174682012-09-14T13:03:00.003-07:002012-09-14T13:05:16.323-07:00To get you started<h3>
1-08-12<br />(Them)</h3>
<div>
<div>
To get you started, you'll need to get an account on Open-DO forge and join the project Hi-Lite:</div>
<div>
<br /></div>
<div>
- go to https://forge.open-do.org/ and create a new account</div>
<div>
- when this is accepted, log in and ask to join project Hi-Lite on</div>
<div>
https://forge.open-do.org/projects/hi-lite/</div>
<div>
- when this is accepted, clone the git repository:</div>
<div>
git clone --recursive git+ssh://developername@scm.forge.open-do.org//scmrepos/git/hi-lite/hi-lite.git</div>
<div>
- note that you can upload your SSH key to avoid typing your password</div>
<div>
each time you access the remote repository (go to MyPage menu, then</div>
<div>
AccountMaitenance, then at the bottom EditKeys)</div>
<div>
<br /></div>
<div>
If you need help with git, don't hesitate to ask. You can also look at this book online: http://git-scm.com/book (chapter 2 is enough)</div>
<div>
<br /></div>
<div>
You should restrict your commits to the directory hi-lite/libs/containers/ada which already contains the version of formal containers developed by Claire Dross. If you've not done it yet, you should read the sections 1 and 2 of her paper "Correct Code Containing Containers" (http://www.open-do.org/wp-content/uploads/2011/06/Correct_Code_Containing_Containers.pdf) that explain what is different between these "formal" containers and the usual ones. I propose that you create a sub-directory inside hi-lite/libs/containers/ada for each family of formal containers on which you'll work.</div>
</div>
<div>
<br /></div>
<h3>
3-08-12<br />(I)</h3>
<div>
<div>
I had already installed gtat gpl and gnat-coll</div>
<div>
gnatls -v</div>
<div>
<br /></div>
<div>
GNATLS GPL 2012 (20120509)</div>
<div>
Copyright (C) 1997-2012, Free Software Foundation, Inc.</div>
<div>
<br /></div>
<div>
Source Search Path:</div>
<div>
<Current_Directory></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/adainclude/</div>
<div>
<br /></div>
<div>
<br /></div>
<div>
Object Search Path:</div>
<div>
<Current_Directory></div>
<div>
/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/adalib/</div>
<div>
<br /></div>
<div>
<br /></div>
<div>
Project Search Path:</div>
<div>
<Current_Directory></div>
<div>
/usr/gnat/i686-pc-linux-gnu/lib/gnat</div>
<div>
/usr/gnat/share/gpr</div>
<div>
/usr/gnat/lib/gnat</div>
<div>
<br /></div>
<div>
[panzon@baleada hi-lite]$ </div>
<div>
<br /></div>
<div>
but I have a doubt cause in the hi-lite/build_instructions.txt (HI-LITE BUILD INSTRUCTIONS FOR ADACORE DEVELOPERS)</div>
<div>
on 2.2) I had the same alt-ergo messages</div>
<div>
<br /></div>
<div>
git submodule init</div>
<div>
[panzon@baleada hi-lite]$ git submodule update</div>
<div>
fatal: Needed a single revision</div>
<div>
Unable to find current revision in submodule path 'alt-ergo'</div>
<div>
<br /></div>
<div>
And then on 3) I don't gnat pro and also you didn't said me anything about Ocaml</div>
<div>
<br /></div>
<div>
So that made me think that maybe I'm doing wrong things</div>
<div>
<br /></div>
<div>
<br /></div>
<div>
by the other hand, I already read the article and I searched some books on my university but we don't have anything about ada 2012, (perhaps no book has been published in 2012 http://en.wikibooks.org/wiki/Ada_Programming/Ada_2012)</div>
<div>
The best book I could find was Programing in Ada 95, Jhon Barnes Addison Wesley</div>
<div>
If you have a better reference please let me know.</div>
<div>
<br /></div>
<div>
I don't know what is the .gpr I had to use</div>
<div>
or maybe I have to write a new one.</div>
</div>
tlakatziEuroñerohttp://www.blogger.com/profile/11597687088698041136noreply@blogger.com0tag:blogger.com,1999:blog-5617837981314980165.post-50730835604343214702012-09-14T13:00:00.002-07:002012-09-14T13:00:35.566-07:00a proposed work breakdown for the internship<h3>
<b>1-08-12</b></h3>
<h3>
<b><br /></b><b>(Them)</b></h3>
<br />
Here is a proposed work breakdown for the internship:<br />
<br />
0. Read the section of the Ada reference manual on containers (http://www.ada-auth.org/standards/12rm/html/RM-A-18.html). It can be useful also that you have a look at the implementation of the Ada standard container library in GNAT. You can get access to it in the GNAT GPL 2012 release (see libre.adacore.com to download it). After installation, just type 'gnatls -v' in a shell and it will give you the Search Path for the standard includes. Here is the complete list of units (the ads for spec, and there is course a corresponding adb for the body) for the standard Ada containers. On the left this is the name that you would expect, and on the right the actual name (due to some constraint on filenames in early DOS systems, all run-time library units have an 8-character name).<br />
<br />
Vectors:<br />
ada-containers-bounded_vectors.ads -> a-cobove.ads<br />
ada-containers-formal_vectors.ads -> a-cofove.ads<br />
ada-containers-indefinite_vectors.ads -> a-coinve.ads<br />
ada-containers-vectors.ads -> a-convec.ads<br />
<br />
Lists:<br />
ada-containers-bounded_doubly_linked_lists.ads -> a-cbdlli.ads<br />
ada-containers-doubly_linked_lists.ads -> a-cdlili.ads<br />
ada-containers-formal_doubly_linked_lists.ads -> a-cfdlli.ads<br />
ada-containers-indefinite_doubly_linked_lists.ads -> a-cidlli.ads<br />
ada-containers-restricted_doubly_linked_lists.ads -> a-crdlli.ads<br />
<br />
Hashed sets:<br />
ada-containers-bounded_hashed_sets.ads -> a-cbhase.ads<br />
ada-containers-formal_hashed_sets.ads -> a-cfhase.ads<br />
ada-containers-hashed_sets.ads -> a-cohase.ads<br />
ada-containers-indefinite_hashed_sets.ads -> a-cihase.ads<br />
<br />
Ordered sets:<br />
ada-containers-bounded_ordered_sets.ads -> a-cborse.ads<br />
ada-containers-formal_ordered_sets.ads -> a-cforse.ads<br />
ada-containers-indefinite_ordered_sets.ads -> a-ciorse.ads<br />
ada-containers-ordered_sets.ads -> a-coorse.ads<br />
<br />
Ordered multisets:<br />
ada-containers-indefinite_ordered_multisets.ads -> a-ciormu.ads<br />
ada-containers-ordered_multisets.ads -> a-coormu.ads<br />
<br />
Hashed maps:<br />
ada-containers-bounded_hashed_maps.ads -> a-cbhama.ads<br />
ada-containers-formal_hashed_maps.ads -> a-cfhama.ads<br />
ada-containers-hashed_maps.ads -> a-cohama.ads<br />
ada-containers-indefinite_hashed_maps.ads -> a-cihama.ads<br />
<br />
Ordered maps:<br />
ada-containers-bounded_ordered_maps.ads -> a-cborma.ads<br />
ada-containers-formal_ordered_maps.ads -> a-cforma.ads<br />
ada-containers-indefinite_ordered_maps.ads -> a-ciorma.ads<br />
ada-containers-ordered_maps.ads -> a-coorma.ads<br />
<br />
1. Augment the existing formal containers with functions corresponding to the procedures:<br />
Replace_Element<br />
Insert<br />
Replace<br />
Delete<br />
Include<br />
Exclude<br />
The goal is to be able to say, for example, that in postcondition of the procedure Replace_Element, the input and output containers are related by the function Replace_Element:<br />
<br />
procedure Replace_Element<br />
(Container : in out Map;<br />
Position : Cursor;<br />
New_Item : Element_Type)<br />
with<br />
Post => Container = Replace_Element (Container'Old, Position, New_Item);<br />
<br />
Of course, there is not much benefit here. The real benefit is when the user can use these functions on his own code to specify the behavior of some programs.<br />
<br />
2. Add contracts (pre- and postconditions) to the Ada formal containers, based on the contracts written by Claire on the intermediate Why3 representation. You will have to look at the containers/why repository to see these existing contracts, and we'll probably need to discuss live before you start on this.<br />
<br />
3. Develop a library of unbounded formal containers. Right now, the library developed by Claire is bounded: when defining a container, the user must declare a fixed maximal size, which is statically allocated, for example:<br />
<br />
L : List(100); -- at most 100 elements in this list<br />
<br />
We'd like to have another library that allows dynamically resizing the containers, like it is done in the standard Ada container library. Of course, this library will need to use dynamic allocation.<br />
<br />
4. Develop a library of bounded and unbounded indefinite formal containers. That is, containers which can hold elements of an indefinite type (= unknown size). This is in particular the case for the classwide types like T'Class. So this library would make it possible to have containers of classwide objects on which the user could call dispatching subprograms. We'll need to discuss more before you start on that.<br />
tlakatziEuroñerohttp://www.blogger.com/profile/11597687088698041136noreply@blogger.com0