From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,48872198fdca5efd,start X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!postnews.google.com!z28g2000vbl.googlegroups.com!not-for-mail From: Maciej Sobczak Newsgroups: comp.lang.ada Subject: SPARK - refactoring and refinement of own state Date: Thu, 20 Aug 2009 00:18:51 -0700 (PDT) Organization: http://groups.google.com Message-ID: <4cc6e9da-9a4a-4a9a-8748-4c5c4a3e9362@z28g2000vbl.googlegroups.com> NNTP-Posting-Host: 137.138.182.236 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: posting.google.com 1250752732 31281 127.0.0.1 (20 Aug 2009 07:18:52 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Thu, 20 Aug 2009 07:18:52 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: z28g2000vbl.googlegroups.com; posting-host=137.138.182.236; posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.1.2) Gecko/20090729 Firefox/3.5.2,gzip(gfe),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:7896 Date: 2009-08-20T00:18:51-07:00 List-Id: I have a problem that can be reduced to a simple hello world program in SPARK. Consider the following: with Spark_IO; --# inherit Spark_IO; --# main_program; procedure Hello --# global in out Spark_IO.Outputs; --# derives Spark_IO.Outputs from *; is begin Spark_IO.Put_String (File => Spark_IO.Standard_Output, Item => "Hello ", Stop => 0); end Hello; Let's suppose that I want to refactor it a bit and move the details of printing to some other package and use that other package from the main program. In other words, I want to isolate the main program from Spark_IO. Consider this package spec: package Greetings --# own State; --# initializes State; is procedure Say_Hello; --# global in out State; --# derives State from *; end Greetings; The main program then becomes: with Greetings; --# inherit Greetings; --# main_program; procedure Hello --# global in out Greetings.State; --# derives Greetings.State from *; is begin Greetings.Say_Hello; end Hello; The SPARK Examiner is happy with both the main program and the spec for the Greetings package. The problem is with the package body. This is what I believe should work: with Spark_IO; --# inherit Spark_IO; package body Greetings --# own State is Spark_IO.Outputs; is procedure Say_Hello --# global in out Spark_IO.Outputs; --# derives Spark_IO.Outputs from *; is begin Spark_IO.Put_String (File => Spark_IO.Standard_Output, Item => "Hello ", Stop => 0); end Say_Hello; end Greetings; However, the examiner says: 4 package body Greetings ^ *** Syntax Error : No DOTTED_SIMPLE_NAME can start with reserved word "BODY". What is most interesting is that after removing the inherit clause from the package body the examiner no longer complains about the "body" keyword, but of course fails later on with the "Spark_IO" procedure prefix, which is reported as undeclared or not visible (semantic error 142). The whole problem is really about refining the own state of some package in terms of the abstract own state of some other package. I have not found anything about this in the SPARK documentation and the error message about the "body" keyword is confusing. Am I going in the right direction anyway? Is this kind of refactoring and refinement possible? -- Maciej Sobczak * www.msobczak.com * www.inspirel.com Database Access Library for Ada: www.inspirel.com/soci-ada