[Spark] Arrays of Strings

[Spark] Arrays of Strings

[Lutz Donnerhacke]

In order to implement thin an execve binding, I wonder how to emulate the
C-Type "char const * const x []". Any bright ideas?

Re: [Spark] Arrays of Strings

[Martin Krischik]

On Tue, 08 Apr 2003 12:02:09 +0000, Lutz Donnerhacke wrote:

> In order to implement thin an execve binding, I wonder how to emulate the
> C-Type "char const * const x []". Any bright ideas?

Depends if you need a 1 to 1 emulation or you want a more high level OO
aproach.

With Regards

Martin

-- 
Martin Krischik
mailto://Martin@krischik.com
http://www.ada.krischik.com

Re: [Spark] Arrays of Strings

[Eric G. Miller]

In <slrnb95ehu.ob.lutz@taranis.iks-jena.de>, Lutz Donnerhacke wrote:

> In order to implement thin an execve binding, I wonder how to emulate the
> C-Type "char const * const x []". Any bright ideas?

Errm, my local definition of execve looks like:

int execve(const char *filename, 
           char *const argv [], char *const envp[]);

What'd the const pointer be for?  Even if your definition had such, that'd
be a burden upon the C function, but shouldn't much affect the Ada side of
things.

Try the following out (rename "/tmp/hello" as appropriate)...

-- executor.ads
with Interfaces.C.Strings;

package Executor is

   package C renames Interfaces.C;

   function Execve (Filename : C.Strings.Chars_Ptr;
                    Argv     : C.Strings.Chars_Ptr_Array;
                    Envp     : C.Strings.Chars_Ptr_Array) return C.Int;

   pragma Import (Convention => C,
                  Entity => Execve,
                  External_Name => "execve");

end Executor;


-- try_exec.adb
with Ada.Text_Io;
use Ada.Text_Io;
with Executor;
with Interfaces.C.Strings;

procedure Try_Exec
is
   package C renames Interfaces.C;

   Argv : C.Strings.Chars_Ptr_Array :=
     (C.Strings.New_String("John"),
      C.Strings.New_String("Bill"),
      C.Strings.New_String("Bob"),
      C.Strings.Null_Ptr);

   -- GNAT says there can't only be one??
   Envp : C.Strings.Chars_Ptr_Array :=
     (C.Strings.Null_Ptr, C.Strings.Null_Ptr);

   FileName : C.Strings.Chars_Ptr :=
     C.Strings.New_String("/tmp/hello");

   Status : C.Int;

begin

   Status := Executor.Execve(FileName => FileName,
                    Argv => Argv, Envp => Envp);

   -- Got here?
   Put_Line ("That didn't work! Got " & C.Int'Image(Status));

end Try_Exec;

-- hello.c
#include <stdio.h>

int main (int argc, char *argv[])
{
  int i;

  for (i = 0; i < argc; ++i) {
    printf ("Hello %s!\n", argv[i]);
  }

  return 0;
}

-- 
echo ">gra.fcw@2ztr< eryyvZ .T pveR" | rot13 | reverse

Re: [Spark] Arrays of Strings

[Lutz Donnerhacke]

* Eric G. Miller wrote:
> In <slrnb95ehu.ob.lutz@taranis.iks-jena.de>, Lutz Donnerhacke wrote:
> 
>> In order to implement thin an execve binding, I wonder how to emulate the
>> C-Type "char const * const x []". Any bright ideas?
> 
> Errm, my local definition of execve looks like:
> 
> int execve(const char *filename, 
>            char *const argv [], char *const envp[]);
> 
> What'd the const pointer be for?  Even if your definition had such, that'd
> be a burden upon the C function, but shouldn't much affect the Ada side of
> things.

"char const * const []" is an array of constant pointers to constant chars.
The modifier const is a postfix modifier. For the first element an
equivalent prefix notation exists for syntactic shugar.

> Try the following out (rename "/tmp/hello" as appropriate)...
> 
> with Ada.Text_Io;
> with Interfaces.C.Strings;

The use of this packages is not possible in Spark. I need an emulation or
shadow of the package Interfaces.C.Strings.

> use Ada.Text_Io;

"use package" is not allowed in Spark.

>    Argv : C.Strings.Chars_Ptr_Array :=
>      (C.Strings.New_String("John"),
>       C.Strings.New_String("Bill"),
>       C.Strings.New_String("Bob"),
>       C.Strings.Null_Ptr);

This involves dynamic memory, which should be avioded as much as possible in
Spark. Language based dynamic memory management is not supported in Spark.

I hope it's clear, what I expect:

package Interfaces is
end Interfaces;

package Interfaces.C is
   type int is range Integer'First .. Integer'Last; -- has to be correct.
end Interfaces.C;

package Interfaces.C.Strings is
   type Chars_Ptr is private;
   type Chars_Ptr_Array is array (Positive range <>) of Chars_Ptr;
private
   type Chars_Ptr is mod 2**32; -- has to be correct.
end Interfaces.C.Strings;


with Interfaces.C.Strings;
--# inherit Interfaces.C.Strings, Interfaces.C;

package Executor is                                                           
   function Execve (
     Filename : Interfaces.C.Strings.Chars_Ptr;
     Argv     : Interfaces.C.Strings.Chars_Ptr_Array;
     Envp     : Interfaces.C.Strings.Chars_Ptr_Array)
     return Interfaces.C.Int;
   
   pragma Import (Convention => C,                                            
     Entity => Execve,                                           
     External_Name => "execve");                                 
end Executor;                                                                 

Re: [Spark] Arrays of Strings

[Lutz Donnerhacke]

* Martin Krischik wrote:
> On Tue, 08 Apr 2003 12:02:09 +0000, Lutz Donnerhacke wrote:
>> In order to implement thin an execve binding, I wonder how to emulate the
>> C-Type "char const * const x []". Any bright ideas?
>
> Depends if you need a 1 to 1 emulation or you want a more high level OO
> aproach.

The emulation should be native Spark and to be used in an inlined syscall.
The syscall interface is so thin, that the inlined code prepare the
registers and switch directly to the kernel.

Example:
pragma No_Run_Time;

with Kernel.Processes, Kernel.IO, Kernel.Linux_i86, Addon;
use type Kernel.IO.long;
--# inherit Kernel, Kernel.Processes, Kernel.IO;

--# main_program;
procedure test_kernel
  --# global in out Kernel.State;
  --# derives Kernel.State from Kernel.State;
  is
   pragma Suppress(All_Checks);

   subtype Buffer_Index is Positive range 1 .. 10;
   subtype Buffer is String(Buffer_Index);
   outbuf : Buffer;
   outlast : Natural;
   outwritten : Natural;
   exitcode : Kernel.Processes.exit_code_t;
   
   child : Kernel.Processes.child_data_t;
   res : Kernel.Linux_i86.syscall_result;
begin
   Kernel.Processes.fork(child, res);
   if res.ok then
      if child.child then
	 outbuf := Buffer'(
	   1 => 'C', 2 => 'h', 3 => 'i', 4 => 'l', 5 => 'd',
	   others => ' ');
	 outlast := 5;
      else
	 outbuf := Buffer'(
	   1 => 'M', 2 => 'a', 3 => 's', 4 => 't', 5 => 'e', 6 => 'r',
	   others => ' ');
	 outlast := 6;
      end if;
   else
      outbuf := Buffer'(
	1 => 'E', 2 => 'r', 3 => 'r', 4 => 'o', 5 => 'r',
	others => ' ');
      outlast := 5;
   end if;
   
   outlast := outlast + 1;
   outbuf(outlast) := ASCII.LF;

   Kernel.IO.write(Kernel.IO.stdout, outbuf, outlast, outwritten, res);
   if not res.ok or else outwritten /= outlast then
      exitcode := 1;
   else
      exitcode := 0;
   end if;
   
   Kernel.Processes.sysexit(exitcode);
end test_kernel;

00000000 <_ada_test_kernel>:
   0:	55                   	push   %ebp
   1:	b8 02 00 00 00       	mov    $0x2,%eax    <= the fork call.
   6:	57                   	push   %edi
   7:	56                   	push   %esi
   8:	53                   	push   %ebx
   9:	83 ec 54             	sub    $0x54,%esp
   c:	cd 80                	int    $0x80        <= the fork call.
   e:	31 db                	xor    %ebx,%ebx
  10:	89 c1                	mov    %eax,%ecx    <= return code for fork
  12:	83 c0 7c             	add    $0x7c,%eax
  15:	89 4c 24 28          	mov    %ecx,0x28(%esp,1)
  19:	83 f8 7b             	cmp    $0x7b,%eax
  1c:	89 d0                	mov    %edx,%eax
  1e:	0f 96 c3             	setbe  %bl          <= set the error bit
  21:	31 f6                	xor    %esi,%esi    <= the if construct
  23:	30 c0                	xor    %al,%al
  25:	89 c2                	mov    %eax,%edx
  27:	09 da                	or     %ebx,%edx
  29:	31 db                	xor    %ebx,%ebx
  2b:	89 54 24 24          	mov    %edx,0x24(%esp,1)
  2f:	84 d2                	test   %dl,%dl
  31:	74 10                	je     43 <_ada_test_kernel+0x43>
 ...

Re: [Spark] Arrays of Strings

[Hyman Rosen]

Lutz Donnerhacke wrote:
>    pragma Suppress(All_Checks);
>    subtype Buffer_Index is Positive range 1 .. 10;
>    subtype Buffer is String(Buffer_Index);
>    outbuf : Buffer;
>    outlast : Natural;
>       outbuf := Buffer'(
> 	1 => 'E', 2 => 'r', 3 => 'r', 4 => 'o', 5 => 'r',
> 	others => ' ');
>       outlast := 5;
>    end if;
>    
>    outlast := outlast + 1;
>    outbuf(outlast) := ASCII.LF;

My God, but this code is cringe-inducing! Is there really no way
to fill the buffer except with this character indexing stuff?
Not only that, but all checks are suppressed, and a type Natural
variable is being used to index and write into a fixed size buffer.
You are just begging for a buffer overflow error here.

This is what the reliable Spark subset of Ada gives you? I always
figure people are fooling themselves when they claim their languages
give them reliability, but I expected a little more from Ada!

Re: [Spark] Arrays of Strings

[Vinzent Hoefler]

Hyman Rosen <hyrosen@mail.com> wrote:

>Not only that, but all checks are suppressed, and a type Natural
>variable is being used to index and write into a fixed size buffer.
>You are just begging for a buffer overflow error here.

You might read a little bit more about SPARK.

>This is what the reliable Spark subset of Ada gives you?

The reliability is not in the subset like in MISRA-C, it is in the
static analysis. I think, it is called *proof*.


Vinzent.

-- 
Parents strongly cautioned  --  this  posting  is  intended for mature
audiences  over  18.  It  may  contain some material that many parents
would not find suitable for children and may include intense violence,
sexual situations, coarse language and suggestive dialogue.

Re: [Spark] Arrays of Strings

[Hyman Rosen]

Vinzent Hoefler wrote:
> The reliability is not in the subset like in MISRA-C, it is in the
> static analysis. I think, it is called *proof*.

I'll accept that, but the code *looks* hideous.

Re: [Spark] Arrays of Strings

[Vinzent Hoefler]

Hyman Rosen <hyrosen@mail.com> wrote:

>Vinzent Hoefler wrote:
>> The reliability is not in the subset like in MISRA-C, it is in the
>> static analysis. I think, it is called *proof*.
>
>I'll accept that, but the code *looks* hideous.

Perhaps. I'd guess

|Buffer'("Error     ")

*might* work too, but then this makes it a little bit harder to count
the lengths correct again. So, as far as I can see, both would have
slight drawbacks. Depends.


Vinzent.

-- 
Parents strongly cautioned  --  this  posting  is  intended for mature
audiences  over  18.  It  may  contain some material that many parents
would not find suitable for children and may include intense violence,
sexual situations, coarse language and suggestive dialogue.

Re: [Spark] Arrays of Strings

[Hyman Rosen]

Vinzent Hoefler wrote:
> The reliability is not in the subset like in MISRA-C, it is in the
> static analysis. I think, it is called *proof*.

I am starting to be a little disturbed now that I've thought about
this a little more. You seem to be telling me that it's OK to have
variables declared loosely (Natural instead of the array range type)
becuase a program verifier will notice problems regardless. To me,
this seems contrary to to the design of Ada, which emphasizes saying
what you mean using the type system. I've been told here frequently
that Ada's style lends itself to avoiding buffer overflows because
you declare variables that loop over array ranges, and so there is
never an opportunity to go off the end.

I find that the posted code looks very much like something you would
see in C (except for that awful buffer setting stuff).

Re: [Spark] Arrays of Strings

[Matthew Heaney]

Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb95ehu.ob.lutz@taranis.iks-jena.de>...
> In order to implement thin an execve binding, I wonder how to emulate the
> C-Type "char const * const x []". Any bright ideas?

Realize that an array in C "decays" to a pointer to the first element,
so x has the type

  const char* const*

If you want to use the char* type in Interfaces.C.Strings, then your
problem reduces to:

  type chars_ptr_access is access constant C.Strings.chars_ptr;
  for chars_ptr_access'Storage_Size use 0;
  pragma Convention (C, chars_ptr_access);

Now just declare an array of aliased chars_ptr, e.g.

  type chars_ptr_array is (Natural range <>) of aliased chars_ptr;
  pragma Convention (C, chars_ptr_array);

  argv_array : constant chars_ptr_array := ...;
  argv_ptr : constant chars_ptr_access := argv_array (0)'Access;

  execv(filename, argv_ptr);


Interestingly, the chars_ptr_array declared in RM95 B.3.1 (6) does not
declare its component subtype as aliased, nor is the array marked as
begin C-compatible.  This seems wrong to me, which is why I declared
the chars_ptr_array type myself, as above.

Re: [Spark] Arrays of Strings

[Matthew Heaney]

"Eric G. Miller" <egm2@Jay-Pee-eSs.net> wrote in message news:<pan.2003.04.09.07.50.03.727731@Jay-Pee-eSs.net>...
> 
> Try the following out (rename "/tmp/hello" as appropriate)...
> 
> -- executor.ads
> with Interfaces.C.Strings;
> 
> package Executor is
> 
>    package C renames Interfaces.C;
> 
>    function Execve (Filename : C.Strings.Chars_Ptr;
>                     Argv     : C.Strings.Chars_Ptr_Array;
>                     Envp     : C.Strings.Chars_Ptr_Array) return C.Int;
> 
>    pragma Import (Convention => C,
>                   Entity => Execve,
>                   External_Name => "execve");
> 

The problem is that C.Strings.chars_ptr_array isn't necessarily
C-compatible, because the RM doesn't promise that it is.

The other issue is that char_ptr_array is unconstrained, which means
it'll try to pass dope over the interface, which is basically
meaningless.  Instead of passing array (unconstrained) array type,
pass an array access type instead.  A component pointer (here, an
access type that designates type chars_ptr) would work too, as I
showed in my previous post.

Re: [Spark] Arrays of Strings

[Vinzent Hoefler]

Hyman Rosen <hyrosen@mail.com> wrote:

>Vinzent Hoefler wrote:
>> The reliability is not in the subset like in MISRA-C, it is in the
>> static analysis. I think, it is called *proof*.
>
>I am starting to be a little disturbed now that I've thought about
>this a little more.

Thinking never hurted anybody. :)

>You seem to be telling me that it's OK to have
>variables declared loosely (Natural instead of the array range type)

Yes, I noticed that in Lutz' code later myself. My quoting was a
little bit misleading (even to myself), I guess.

But still it had nothing to do with your comments about "subset", I
was thinking more about the "character indexing stuff" you complained
about.

>becuase a program verifier will notice problems regardless.

Although this *might* be true sometimes, it was definitely not my
intention to say such stupid thing.

But sometimes a restricted subset might lead to code that could be
expressed (far) more easily with the original superset of the
language. That was what I was trying to say.

>I've been told here frequently
>that Ada's style lends itself to avoiding buffer overflows because
>you declare variables that loop over array ranges, and so there is
>never an opportunity to go off the end.

This doesn't apply to the code here, because the assignments are quite
static anyway, but generally I'd say, yes, this is right.

Call it experience. :-)

>I find that the posted code looks very much like something you would
>see in C (except for that awful buffer setting stuff).

Well, it's still code interfacing to a C-kernel. ;->

And it was called test_...


Vinzent.

-- 
Parents strongly cautioned  --  this  posting  is  intended for mature
audiences  over  18.  It  may  contain some material that many parents
would not find suitable for children and may include intense violence,
sexual situations, coarse language and suggestive dialogue.

Re: [Spark] Arrays of Strings

[Randy Brukardt]

Hyman Rosen wrote in message <1049908902.143649@master.nyc.kbcfp.com>...
>I find that the posted code looks very much like something you would
>see in C (except for that awful buffer setting stuff).


Ada code intended to interface to directly to C often tends to look like
C - that is, it's ugly, range checking has to be turned off, and so on.
That's why thick bindings like Claw are so important - they hide that
cruft from view so that the majority of your program actually can
benefit from Ada. If you let the C interfacing stuff spread across your
program, you have gained nothing by using Ada.

            Randy.

Re: [Spark] Arrays of Strings

[Randy Brukardt]

Matthew Heaney wrote in message
<1ec946d1.0304090942.3106b4e4@posting.google.com>...
>Interestingly, the chars_ptr_array declared in RM95 B.3.1 (6) does not
>declare its component subtype as aliased, nor is the array marked as
>begin C-compatible.  This seems wrong to me, which is why I declared
>the chars_ptr_array type myself, as above.

This has come up before. See AI-276. (Personally, I think that type
ought to be deleted, as it has nothing to do with the Ada Strings
package - having no operations - and it is easily written by any
programmer that needs it. But that's too radical.)

         Randy.

Re: [Spark] Arrays of Strings

[Lutz Donnerhacke]

* Matthew Heaney wrote:
> Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb95ehu.ob.lutz@taranis.iks-jena.de>...
>> In order to implement thin an execve binding, I wonder how to emulate the
>> C-Type "char const * const x []". Any bright ideas?
>
> Realize that an array in C "decays" to a pointer to the first element,
> so x has the type
> 
>   const char* const*

Known.

> If you want to use the char* type in Interfaces.C.Strings, then your
> problem reduces to:
> 
>   type chars_ptr_access is access constant C.Strings.chars_ptr;
>   for chars_ptr_access'Storage_Size use 0;
>   pragma Convention (C, chars_ptr_access);

Ack. And Spark does not allow access types. So my question is still open.

Re: [Spark] Arrays of Strings

[Matthew Heaney]

Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb9aagi.p2.lutz@taranis.iks-jena.de>...
> * Matthew Heaney wrote:
> 
> > If you want to use the char* type in Interfaces.C.Strings, then your
> > problem reduces to:
> > 
> >   type chars_ptr_access is access constant C.Strings.chars_ptr;
> >   for chars_ptr_access'Storage_Size use 0;
> >   pragma Convention (C, chars_ptr_access);
> 
> Ack. And Spark does not allow access types. So my question is still open.

Doesn't Spark have a #hide clause, to turn off Spark checking?  After
all, you're calling a C library function, so what difference does
Spark make?

You could simply pass type System.Address.

  execv(filename, argv_array (argv_array'First)'Address);

Or you could use an access parameter:

  execv(filename, argv_array (argv_array'First)'Access);

Re: [Spark] Arrays of Strings

[Hyman Rosen]

Matthew Heaney wrote:
> Doesn't Spark have a #hide clause, to turn off Spark checking?  After
> all, you're calling a C library function, so what difference does
> Spark make?

Getting rid of features that are presumed to cause problems is a bit of
hubris that language designers always seem to fall victim to. Ada itself
had a huge problem because the designers thought that function pointers
could be eliminated. Spark gets rid of all pointers, Java gets rid of
templates, and so on and so on.

Then everyone who uses these languages has to figure out how to work
around the lack of the feature they need, essentially duplicating it in
some kludgy way. Meanwhile the language designers have their heads in the
sand and their noses in the air while they pat themselves on the back (:-)
in self-congratulation on how they have created perfection.

Re: [Spark] Arrays of Strings

[Lutz Donnerhacke]

* Matthew Heaney wrote:
> Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb9aagi.p2.lutz@taranis.iks-jena.de>...
>> * Matthew Heaney wrote:
>> > If you want to use the char* type in Interfaces.C.Strings, then your
>> > problem reduces to:
>> >
>> >   type chars_ptr_access is access constant C.Strings.chars_ptr;
>> >   for chars_ptr_access'Storage_Size use 0;
>> >   pragma Convention (C, chars_ptr_access);
>>
>> Ack. And Spark does not allow access types. So my question is still open.
>
> Doesn't Spark have a #hide clause, to turn off Spark checking?  After
> all, you're calling a C library function, so what difference does
> Spark make?

Right, but I'm looking for the Spark frontend of this hide clause.

> You could simply pass type System.Address.

Of course. I can pass any private type, but how do I initialize such a thing?

>   execv(filename, argv_array (argv_array'First)'Address);

This call has to occur in normal Spark.
argv_array has which type? array (Positive range <>) of System.Address?

And the examinder says:
***        Semantic Error    : 54: Illegal attribute: Address.

> Or you could use an access parameter:
>
>   execv(filename, argv_array (argv_array'First)'Access);

How do I do this in a Spark frontend? Of course, I can hide the whole
program, but this is not really a solution.

Re: [Spark] Arrays of Strings

[Hyman Rosen]

Lutz Donnerhacke wrote:
> How do I do this in a Spark frontend? Of course, I can hide the whole
> program, but this is not really a solution.

"Doctor, it hurts when I do that."
"Then don't do that!"

Why have you chosen to work in a language which deliberately
prevents you from expressing what you explicitly need to do?

This whole thing has an air of the naughty Victorians about it.
No one is willing to talk about what they're doing, but they're
all doing it. The program stands there full of hypocrisy, saying
"Pointers? Who me? I'm in Spark! No pointers here!" while dealing
in pointers with its shady C-based friends.

Re: [Spark] Arrays of Strings

[Randy Brukardt]

Hyman Rosen wrote in message <1049989859.683662@master.nyc.kbcfp.com>...
>Lutz Donnerhacke wrote:
>> How do I do this in a Spark frontend? Of course, I can hide the whole
>> program, but this is not really a solution.
>
>"Doctor, it hurts when I do that."
>"Then don't do that!"
>
>Why have you chosen to work in a language which deliberately
>prevents you from expressing what you explicitly need to do?


I hate to do it, but I have to agree with Hyman here.

There is no way to make the code directly interfacing with C any safer
than the underlying C, and that is never going to be anywhere near the
standards of Spark.

What has to be done in cases like this is to write an appropriate thick
wrapper that IS espressible in Spark, and then the ugly interfacing code
has to be in 'real' Ada with the Spark checking turned off.

I don't use Spark, but the Prog_Call function of Janus/Ada (which of
course calls one of the exec functions) has an interface like:

      function Prog_Call (Program_Name : in String;
                                        Command : in String;
                                        Wait : Boolean := True);

and all of the ugly pointer stuff needed to implement that interface is
hidden in the body of the package.

Abstracting the environment variable stuff will be hard (if you actually
need that; it's rare -- Prog_Call just passes null, which is a copy of
the caller's for Windows, I forget what Unix does with that), but I
don't think you have any choice in order to make proper Spark.

The overhead of such a wrapper can be reduced by in-lining and the like,
but it hardly can matter: exec functions are a lot slower than large
volumes of Ada code, and we're certainly not talking about that.

                 Randy.

Re: [Spark] Arrays of Strings

[John R. Strohm]

"Hyman Rosen" <hyrosen@mail.com> wrote in message
news:1049908902.143649@master.nyc.kbcfp.com...
> Vinzent Hoefler wrote:
> > The reliability is not in the subset like in MISRA-C, it is in the
> > static analysis. I think, it is called *proof*.
>
> I am starting to be a little disturbed now that I've thought about
> this a little more. You seem to be telling me that it's OK to have
> variables declared loosely (Natural instead of the array range type)
> becuase a program verifier will notice problems regardless. To me,
> this seems contrary to to the design of Ada, which emphasizes saying
> what you mean using the type system. I've been told here frequently
> that Ada's style lends itself to avoiding buffer overflows because
> you declare variables that loop over array ranges, and so there is
> never an opportunity to go off the end.
>
> I find that the posted code looks very much like something you would
> see in C (except for that awful buffer setting stuff).

Disclaimer: This is not a discussion of SPARK as such, but instead of formal
verification in the general sense.

When you declare an array to be of a given size, you create a proof
obligation that the subscript expression will always be in bounds.
Satisfying this proof obligation is what you do during verification.

Consider

procedure main is
i:integer;
x: array(1..10) of real;
begin
  for i in 2..4 loop
    x(2*i+1) := 0;
  end loop;
end;

The array X is declared to be (1..10).  This generates an obligation that
for all X(<foo>), 1 le <foo> and <foo> le 10.

In this particular case, the verifier must satisfy

for all i:integer, i in 2..4
  --> (implies)
2*i+1 in 1..10

or

for all i:integer, i in 2..4
  -->
2*i in 0..9

or

i in 2..4
  -->
i in 0..4

which is trivially true if your verifier knows how to deal with this kind of
inequality processing.  (That capability has existed since the late 1970s.)
And even if your verifier doesn't understand inequality intervals, it can
exhaustively enumerate all values of i that satisfy the hypothesis and check
that they satisfy the conclusion.  (Some model checkers do that kind of
thing.)

What normally happens is that you will generate a proof obligation that you
may not be able to prove.  This is normal.  Usually, you can't DISPROVE a
proof obligation, you can only fail to find a proof for it.  (There exist
mechanical procedures for finding proofs of theorems, that WILL succeed if a
proof does in fact exist.  They may take a while.)  There are typically two
reasons for this: 1) you haven't brought enough information into context, 2)
you've uncovered a bug.  (There is a third possibility: you've uncovered an
instance of Godel's Theorem, but in practice that doesn't seem to happen.)

Consider

procedure main is
i:integer;
x: array(1..10) of real;
begin
  for i in 2..4 loop
    x(2*i+3) := 0;
  end loop;
end;

The proof obligation will become

i in 2..4 --> 2*i+3 in 1..10
i in 2..4 --> 2*i in -2..7
i in 2..4 --> i in -1..3   *TILT*

At this point, your theorem prover will do something roughly analogous to
throwing up its hands and saying "Beats me, daddy-O".  (With apologies to
Maynard G. Krebs...)  You are expected to look at the problem, look at the
code, and say "DOH!" and fix the obvious error.

Yes, it would be a bit more self-documenting if i were declared to be
integer(1..10), but it doesn't actually matter for verification.

OK, but what if the subscript is coming from somewhere else?

Simple.  Consider

procedure foo(i:integer) is
x:array(1..10) of real;
begin
  x(i) := 42;
end;

Again, a proof obligation is generated, to prove that i is in 1..10.  The
proof obligation must then be propagated to all of the callers of foo, and
proved individually.  Whether that obligation is propagated automatically by
the verification environment, or manually by the programmer adding an entry
specification annotation, is implementation-dependent.  Obviously, either
way will work.

Made-up example:

procedure foo(i:integer) is
x:array(1..10) of real;
entryspec i in 1..10;
begin
  x(i) := 42;
end;

The use of an entry specification generally simplifies the verification of
foo, in that it tells the verifier what it is allowed to assume.  At the
same time, it explicitly generates a proof obligation on the callers of foo.

Re: [Spark] Arrays of Strings

[Chad R. Meiners]

"Hyman Rosen" <hyrosen@mail.com> wrote in message
news:1049986095.779228@master.nyc.kbcfp.com...
> Getting rid of features that are presumed to cause problems is a bit of
> hubris that language designers always seem to fall victim to. Ada itself
> had a huge problem because the designers thought that function pointers
> could be eliminated. Spark gets rid of all pointers, Java gets rid of
> templates, and so on and so on.

You are missing the point of Spark which is to provide a (super)subset of
Ada in which formal proofs about the implementation are possible.  Lack of
pointers was not a case of hubris but a deliberate and sound decision in
Spark's case.  Formal validation and verification methodologies require
unambiguous specifications and implementations.  Spark is intended to
satisfy such formal needs.

> Then everyone who uses these languages has to figure out how to work
> around the lack of the feature they need, essentially duplicating it in
> some kludgy way. Meanwhile the language designers have their heads in the
> sand and their noses in the air while they pat themselves on the back (:-)
> in self-congratulation on how they have created perfection.

Of one should know something about a language before one chooses to
overgeneralize ;)

Re: [Spark] Arrays of Strings

[Chad R. Meiners]

"Lutz Donnerhacke" <lutz@iks-jena.de> wrote in message
news:slrnb9b1r8.p2.lutz@taranis.iks-jena.de...


> Right, but I'm looking for the Spark frontend of this hide clause. );
>
> How do I do this in a Spark frontend? Of course, I can hide the whole
> program, but this is not really a solution.

Couldn't you just create an inlined procedure for each literal call to
execv?
This way you could just hide the execv call in the body while keeping the
rest of your code in Spark.

Re: [Spark] Arrays of Strings

[Phil Thornley]

"Hyman Rosen" <hyrosen@mail.com> wrote in message
news:1049986095.779228@master.nyc.kbcfp.com...
> Getting rid of features that are presumed to cause problems is a bit
of
> hubris that language designers always seem to fall victim to. Ada
itself
> had a huge problem because the designers thought that function
pointers
> could be eliminated. Spark gets rid of all pointers, Java gets rid of
> templates, and so on and so on.
>
> Then everyone who uses these languages has to figure out how to work
> around the lack of the feature they need, essentially duplicating it
in
> some kludgy way. [abuse snipped]

There must be very few SPARK based systems that don't have to include
some non-SPARK code. (One whole chapter of the SPARK book is about
interfacing to such code.)

But to argue that this makes languages such as SPARK wholly useless is
specious.

If I am writing the code for a safety-critical system then all of that
code has to be brought to the same integrity level. If 99% of that is
SPARK code then the effort to validate that code is minimised and I am
quite content to put a lot of manual analysis (per line of code) into
bringing the remaining 1% up to the same integrity level.

Phil Thornley

--
Phil Thornley
BAE SYSTEMS

Re: [Spark] Arrays of Strings

[Lutz Donnerhacke]

* Chad R. Meiners wrote:
> "Lutz Donnerhacke" <lutz@iks-jena.de> wrote in message
>> Right, but I'm looking for the Spark frontend of this hide clause. );
> 
> Couldn't you just create an inlined procedure for each literal call to
> execv?

execv(cmd, arg0);
execv(cmd, arg0, arg1);
execv(cmd, arg0, arg1, arg2);
...

Yep, this is possible, but looks insane.

I'm working on a solution like:

procedure t is 
  argsstring : constant C_String_Collection :=  -- limited type 
    "/usr/bin/sh" & ASCII.NUL & "-c" & ASCII.NUL & "xxx" & ASCII.NUL;   
  args : C_String_Array;                  -- contains address of collection
  envstring : Enviroment_Collection(1 .. 400); 
  env : Enviroment;   
begin     
  Array_From_Collection(argsstring, args);     

  Bind_Enviroment(envstring, env);        
  Add_Enviroment("HOME", "/var/home/lutz");          
  Add_Enviroment("USER", "lutz");            
  
  execve(To_Fullpath("/usr/bin/sh"), args, env);               
end t;                 
		

Re: [Spark] Arrays of Strings

[Marin David Condic]

I can agree with Hyman's point to some extent. Trying to eliminate all
possible sources of errors via language design is not going to work and only
succeeds in making the language less useful in solving problems. (Sort of
like trying to teach a pig to dance - it doesn't work and only succeeds in
annoying the pig. :-) There isn't really any substitute for solid design and
rigorous testing if you want a stable, reliable end product. A "safe"
language can lead developers to find ugly, difficult ways around the safety
features in order to get what the designers wanted out of the system.

OTOH, there is some value in something like SPARK wherein one can substitute
formal proof of correctness for formal verification by testing. Verification
can be very time consuming. Some features can make it difficult or
impossible to to test an end product and have a high level of confidence
that the end product will not break. To the extent that the formal proof is
faster and more dependable than formal verification, it gets you a better
product in a less costly way - hence your point about the value of SPARK for
a large percentage of the code and other verification methods for the
smaller percentage.

Its all a balancing act. I believe that the safety features of Ada are a
good thing and hence I agree that SPARK can be a good thing too. But a
desire for absolute safety can end up hamstringing a language and you'll
never get the absolute safety anyway. One would hope that language designers
would keep this in mind and look to the target audience to see what features
are useful as well as what features are safe.

MDC
--
======================================================================
Marin David Condic
I work for: http://www.belcan.com/
My project is: http://www.jsf.mil/

Send Replies To: m c o n d i c @ a c m . o r g

    "Going cold turkey isn't as delicious as it sounds."
        -- H. Simpson
======================================================================

Phil Thornley <phil.thornley@baesystems.com> wrote in message
news:3e966fc9$1@baen1673807.greenlnk.net...
>
> There must be very few SPARK based systems that don't have to include
> some non-SPARK code. (One whole chapter of the SPARK book is about
> interfacing to such code.)
>
> But to argue that this makes languages such as SPARK wholly useless is
> specious.
>
> If I am writing the code for a safety-critical system then all of that
> code has to be brought to the same integrity level. If 99% of that is
> SPARK code then the effort to validate that code is minimised and I am
> quite content to put a lot of manual analysis (per line of code) into
> bringing the remaining 1% up to the same integrity level.
>

Re: [Spark] Arrays of Strings

[Hyman Rosen]

John R. Strohm wrote:
> When you declare an array to be of a given size, you create a proof
> obligation that the subscript expression will always be in bounds.
> Satisfying this proof obligation is what you do during verification.


Sure, I understand what program proof and verification are about.

What I'm suggesting is that there is a tension between normal Ada
usage, which is to declare your types "snugly" so that they hold
only the ranges you expect them to have, and programs which will
always be verified before they are permitted to run.

Re: [Spark] Arrays of Strings

[Hyman Rosen]

Chad R. Meiners wrote:
> You are missing the point of Spark which is to provide a (super)subset of
> Ada in which formal proofs about the implementation are possible.  Lack of
> pointers was not a case of hubris but a deliberate and sound decision in
> Spark's case.  Formal validation and verification methodologies require
> unambiguous specifications and implementations.  Spark is intended to
> satisfy such formal needs.

I think you are demonstrating *my* point. Despite the intentions of Spark,
the OP needs to generate and pass a pointer, and he's desperately trying
to work around the constraints of his programming language. It's all good
and well that you can verify programs written in Spark, but it's not of
much use if programs written in Spark can't do anything!

>>Then everyone who uses these languages has to figure out how to work
>>around the lack of the feature they need, essentially duplicating it in
>>some kludgy way. Meanwhile the language designers have their heads in the
>>sand and their noses in the air while they pat themselves on the back (:-)
>>in self-congratulation on how they have created perfection.
> 
> Of one should know something about a language before one chooses to
> overgeneralize ;)

Do you remember how, in the days of Ada83, it would be suggested that
people use task types and pointers to them to work around the lack of
procedure pointers? Overgeneralize, my foot!

Re: [Spark] Arrays of Strings

[Rod Chapman]

Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb95ehu.ob.lutz@taranis.iks-jena.de>...
> In order to implement thin an execve binding, I wonder how to emulate the
> C-Type "char const * const x []". Any bright ideas?


Lutz and others,
  Here are some thoughts and a possible solution to this problem.
The execve() API is indeed a complex one for SPARK, since the
type "pointer to unconstrained array of pointer to null terminated
C String" is a tricky one for SPARK to model.

 The trick with bindings like this is to come up with a package
specification which is pure SPARK, and presents a clean,
elegant model to the outside world.  No details of the
C type model, or the "glue" needed to bind the two languages
together should be allowed to leak into the package spec!
All the glue and C-related stuff should be hidden in the body.

I'm also working on the assumption that Lutz wants a binding
that is as "thin" as possible, and there are good reasons
to support this approach.

Let's look at how the GNAT.OS_Lib does it...a few fragments:

   type String_Access is access all String;
   type String_List is array (Positive range <>) of String_Access;
   subtype Argument_List is String_List;

   procedure Spawn
     (Program_Name : String;
      Args         : Argument_List;
      Success      : out Boolean);

OK - reasonably elegant, but unfortunately not much use
in this context, since SPARK does not allow explicit declaration
of access types.

The trick here (thanks to Tucker Taft here, who just thought of this
during lunch...) is to change the abstraction a bit to make the
"Args" parameter a legal SPARK type...

I suggest using a single String parameter, where distinct arguments
are separated and terminated by a special character.  ASCII.Nul
is probably a good choice!

So...the SPARK-friendly package spec looks something like:

  package Kernel
  --# own State;
  --# initializes State;
  is
     -- "Args" is a list of arguments, each of which is
     -- termianted by ASCII.Nul
     --
     -- For Example
     --   Kernel.Spawn (Program_Name => "gcc",
     --                 Args         => "-c" & ASCII.Nul &
     --                                 "-g" & ASCII.Nul &
     --                                 "spark.adb" & ASCII.Nul,
     --                 Success      => Success);

     procedure Spawn (Program_Name : in     String;
                      Args         : in     String;
                      Success      :    out Boolean);
     --# global in out State;
     --# derives Success from State, Program_Name, Args &
     --#         State from *, Program_Name, Args;

  end Kernel;

This meets our requirements - perfectly legal SPARK, and none of the
C-related glue is visible.

The body is Ada95 (not SPARK), and uses the facilities of Annex B and
Interfaces to do its stuff.  I've left out a few details but it
goes something like:

   with Interfaces;
   with Interfaces.C;
   with Interfaces.C.Strings;
   use type Interfaces.C.Char;
   use type Interfaces.C.Size_T;
   use type Interfaces.C.Int;
   package body Kernel
   is

     package C renames Interfaces.C;

     -- Count the number of Nul-terminated argments in a given
String...
     function Number_of_Args (Args : in String) return C.Size_T
     is
     begin
       return 2;
     end Number_of_Args;

     procedure Spawn (Program_Name : in     String;
                      Args         : in     String;
                      Success      :    out Boolean)
     is
        subtype Args_Count is C.size_t range 1 .. Number_Of_Args
(Args);
        type Args_Ptr_Vector is array (Args_Count) of aliased
C.Strings.Chars_Ptr;
        Args_Ptrs      : Args_Ptr_Vector;

        subtype C_Args_Index is C.size_t range C.Size_T(Args'First) ..
C.Size_T(Args'Last);
        subtype C_Args_Type  is C.char_array (C_Args_Index);
        C_Args         : C_Args_Type := C.To_C (Args, False);

        C_Program_Name : C.Strings.chars_ptr;
        Ret            : C.Int;

        -- Bind to C here - I've missed out envp here for
simplicity...
        function Execve (Filename : in C.Strings.Chars_Ptr;
                         Argv     : in C.Strings.Chars_Ptr) return
C.Int;
        pragma Import (C, Execve);

        -- Sets the elements of Args_Ptrs to be the 'Access
        -- of each of the N arguments contained in C_Args...
        procedure Set_Args_Ptrs
        --# global out Args_Ptrs;
        --#        in  C_Args;
        is
        begin
           -- proof left to reader... :-)
           null;
        end Set_Args_Ptrs;


     begin
        C_Args := C.To_C (Args, False);

        Set_Args_Ptrs;

        C_Program_Name := C.Strings.New_String (Program_Name);

        Ret := Execve (C_Program_Name, Args_Ptrs (1)'Access);

        C.Strings.Free (C_Program_Name);

        Success := (Ret = 0); -- or something like that...
     end Spawn;
  end Kernel;

Re: [Spark] Arrays of Strings

[John R. Strohm]

"Hyman Rosen" <hyrosen@mail.com> wrote in message
news:1050063540.619475@master.nyc.kbcfp.com...
> John R. Strohm wrote:
> > When you declare an array to be of a given size, you create a proof
> > obligation that the subscript expression will always be in bounds.
> > Satisfying this proof obligation is what you do during verification.
>
>
> Sure, I understand what program proof and verification are about.
>
> What I'm suggesting is that there is a tension between normal Ada
> usage, which is to declare your types "snugly" so that they hold
> only the ranges you expect them to have, and programs which will
> always be verified before they are permitted to run.

Nope.

Declaring the types "snugly" is a good idea.  It gives more information to
the compiler and to the verification system.  It may OR MAY NOT make the
verification easier.
The point is that it is not mandatory: the verification system can figure
out the actual constraints.

Declaring the types "snugly" may make the verification harder.  Every time a
snugly-declared variable is assigned, a proof obligation is generated, to
prove that the variable will be in bounds.  Some of these obligations will
be trivial; some may not be.

Re: [Spark] Arrays of Strings

[John R. Strohm]

"Marin David Condic" <mcondic.auntie.spam@acm.org> wrote in message
news:b76b3a$slo$1@slb9.atl.mindspring.net...
> I can agree with Hyman's point to some extent. Trying to eliminate all
> possible sources of errors via language design is not going to work and
only
> succeeds in making the language less useful in solving problems. (Sort of
> like trying to teach a pig to dance - it doesn't work and only succeeds in
> annoying the pig. :-) There isn't really any substitute for solid design
and
> rigorous testing if you want a stable, reliable end product. A "safe"
> language can lead developers to find ugly, difficult ways around the
safety
> features in order to get what the designers wanted out of the system.

"Testing cannot be used to show the absence of errors, only their
resence."  --Edsger W. Dijkstra

Yes, you can force some ugly and difficult workarounds for lack of e.g.
pointers and GOTO statements.

HOWEVER, no matter how ugly and difficult those workarounds may be, they are
known to be SAFE.  The simple, easy-to-use constructs they replaced were NOT
SAFE.

Secondly, the presence of those ugly, difficult workarounds draws the
maintenance programmer's eye, alerting him that there are demons and tygers
lurking hereabouts.  This is PRECISELY why Ada made the GOTO label syntax
INCREDIBLY ugly: they were required by the customer to provide a GOTO
statement, but they could, and did, warn against its use.

Re: [Spark] Arrays of Strings

[Peter Amey]

Rod Chapman wrote:
> Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb95ehu.ob.lutz@taranis.iks-jena.de>...
> 
[Rod's solution snipped]

The crucial thing about all this is that the nasty details of 
interfacing to the dubious C interface are all contrained to a thin 
layer in the package body.  Outside this interface we have a nice clean 
link to the rather purer world of SPARK.

I tend to se this in the same light as Ada's view of things like 
unchecked conversion: it's allowed but we have to be open and explicit 
about what we are doing.

Peter

Re: [Spark] Arrays of Strings

[Chad R. Meiners]

"Hyman Rosen" <hyrosen@mail.com> wrote in message
news:1050064265.685430@master.nyc.kbcfp.com...

> I think you are demonstrating *my* point.

No I am not.  You are not listening to the argument and questioning your own
opinion.

> Despite the intentions of Spark,
> the OP needs to generate and pass a pointer, and he's desperately trying
> to work around the constraints of his programming language.

As Rod Chapman and Peter Amey point out, the data type the OP is worrying
needs to be modeled in Spark-friendly way that can used to accomplish the
actually call in the none Spark body.  As for trying desperately to work
around the constraints of Spark, I also believe that you misunderstood the
OP.  It is my opinion he was trying to get advice on how to work with the
language constraint so that he could separate the provable part of the
program for the part left unproven.  So the OP might have been frustrated
but learning usually involves some frustration due to misunderstandings of
lack of knowledge.

> It's all good
> and well that you can verify programs written in Spark, but it's not of
> much use if programs written in Spark can't do anything!

This is a ludicrous argument.  Of course you can useful programs in Spark
(been done with published case studies see www.sparkada.com).  The nice
point about Spark is that you can only apply it where necessary and
interface it cleanly to the rest of your Ada code base (thus you can also
interface to other programming languages as well)

> Do you remember how, in the days of Ada83, it would be suggested that
> people use task types and pointers to them to work around the lack of
> procedure pointers?

You are distracting from the argument.  The above is irrelevant.

> Overgeneralize, my foot!

Of course you overgeneralized!  The design process and goals of Java and
Spark are unrelated and you cannot attribute any perceived language faults
out of either to the same process (this vague notion of language design
hubris).  You also presented a strawman argument.  There was no hubris
uninvolved in the creation of Spark.  You should at least read the history
and rational of Spark before you pass judgment upon its designers hubris.
Spark does not pretend to provide you with all the capabilities of most
general purpose programming languages.  It instead realized that some code
is going to have to exist outside the Spark boundary and provides you with a
nice method to interface with this code.  This is a very nice feature since
it allows you to explicitly state where you are separating your concerns.
This is not hubris but instead a very good idea!

You must also remember that Spark is a formal method.  Learning formal
methodologies require a `slight' paradigm change on your developmental
thinking.  This is why they are often misunderstood and mischaracterized by
strawman arguments.

Re: [Spark] Arrays of Strings

[Matthew Heaney]

rod.chapman@praxis-cs.co.uk (Rod Chapman) wrote in message news:<cf2c6063.0304110211.596b6b2b@posting.google.com>...
> Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb95ehu.ob.lutz@taranis.iks-jena.de>...
> > In order to implement thin an execve binding, I wonder how to emulate the
> > C-Type "char const * const x []". Any bright ideas?
> 
> 
> Lutz and others,
>   Here are some thoughts and a possible solution to this problem.
> The execve() API is indeed a complex one for SPARK, since the
> type "pointer to unconstrained array of pointer to null terminated
> C String" is a tricky one for SPARK to model.

[Rod's example snipped]

Personally, I find Rod's solution way too heavy.

Why can't Spark model an access constant to a constant object?  For
example:

declare
   X : aliased constant String := "arg1";
   Y : aliased constant String := "arg2":

   type String_Constant_Access is 
     access constant String;

   type String_Constant_Access_Array is
     (Postiive range <>) of aliased String_Constant_Access;

   A : constant String_Constant_Access_Array := 
     (X'Access, Y'Access);
begin
   Op (A (A'First)'Access);
end;

Everything is static.  Yes, X and Y are aliased by the components of
array A, but neither X nor Y is variable, and the aliased view through
A is only a constant view.  So what's the problem?

I could understand your difficulty if X and Y were variable, but that
is not the case here.

I must say, I think the simplest solution is:

exec (filename, X);  -- for argv with one arg
exec (filename, X, Y); --for argv with two args
etc

and then turn off Spark checking in the body of exec.

Contrary to some of the views expressed in this thread, I find the C
syntax perfectly natural and perfectly elegant.  Rod's solution is
neither.

Re: [Spark] Arrays of Strings

[Chad R. Meiners]

"Marin David Condic" <mcondic.auntie.spam@acm.org> wrote in message
news:b76b3a$slo$1@slb9.atl.mindspring.net...
> I can agree with Hyman's point to some extent. Trying to eliminate all
> possible sources of errors via language design is not going to work and
only
> succeeds in making the language less useful in solving problems. (Sort of
> like trying to teach a pig to dance - it doesn't work and only succeeds in
> annoying the pig. :-)

If this was Hyman's point, then it one that most people that deal with
formal methods agree with.  Almost all the people that deal with formal
methods understand logic and expressiblity; thus they are not going to
intentional try to eliminate all sources of errors via language design.
That is simple, "My language allow nothing to be expressed".  Of course you
can also go to the opposite extreme, "All things are expressions of my
language".  Both language are useless.   The challenge with formal methods
is to get the balance right with reguards to requirments, specifications and
finally implementations.  In my profesional opinion (formal methods are the
focus of my graduate studies), I think that Spark demonstrates a very good
sense of balance in this respect.

Re: [Spark] Arrays of Strings

[Chad R. Meiners]

"Matthew Heaney" <mheaney@on2.com> wrote in message >
>Personally, I find Rod's solution way too heavy.
>
> Why can't Spark model an access constant to a constant object?  For
> example:

You probably could make rules to allow access constants to constant object,
but why?  Its usefulness would probably be outweighted by its added
complexity.  Furthermore, it would make the language more complicated to
learn.  If you intend on proving result about your implementation, you
should understand the implementation language so you can validate your proof
in respect to your implementations requirements.

> declare
>    X : aliased constant String := "arg1";
>    Y : aliased constant String := "arg2":
>
>    type String_Constant_Access is
>      access constant String;
>
>    type String_Constant_Access_Array is
>      (Postiive range <>) of aliased String_Constant_Access;
>
>    A : constant String_Constant_Access_Array :=
>      (X'Access, Y'Access);
> begin
>    Op (A (A'First)'Access);
> end;
>
> Everything is static.  Yes, X and Y are aliased by the components of
> array A, but neither X nor Y is variable, and the aliased view through
> A is only a constant view.  So what's the problem?

I would assume that the value added does not offset the cost to provide.

> I must say, I think the simplest solution is:
>
> exec (filename, X);  -- for argv with one arg
> exec (filename, X, Y); --for argv with two args
> etc
>

How is that so much different from Spawn(filename, X & Seperator & Y,
MySuccess); ?

> and then turn off Spark checking in the body of exec.
>
> Contrary to some of the views expressed in this thread, I find the C
> syntax perfectly natural and perfectly elegant.  Rod's solution is
> neither.

Rod's solution is correct though; furthermore, it isn't too heavy since all
the work in deciding what needs to be proved and what will be left unproved
needs to be done explicitly one way or the other.

Re: [Spark] Arrays of Strings

[Peter Amey]

Matthew Heaney wrote:
> rod.chapman@praxis-cs.co.uk (Rod Chapman) wrote in message news:<cf2c6063.0304110211.596b6b2b@posting.google.com>...
> 
>>Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb95ehu.ob.lutz@taranis.iks-jena.de>...
>>
>>>In order to implement thin an execve binding, I wonder how to emulate the
>>>C-Type "char const * const x []". Any bright ideas?
>>
>>
>>Lutz and others,
>>  Here are some thoughts and a possible solution to this problem.
>>The execve() API is indeed a complex one for SPARK, since the
>>type "pointer to unconstrained array of pointer to null terminated
>>C String" is a tricky one for SPARK to model.
> 
> 
> [Rod's example snipped]
> 
 >
 > [Mathew Heaney...]
> Personally, I find Rod's solution way too heavy.
> 
> Why can't Spark model an access constant to a constant object?  For
> example:
> 

The answer is it probably _could_ (but whether it _should_ is a much 
closer value judgement).  In fact we are looking very seriously at 
"static" access discriminants as part of our work on adding the 
Ravenscar tasking profile to SPARK. (We have a working Ravenscar SPARK 
already without this feature).

We have never claimed that SPARK is the largest subset of Ada for which 
formal verification is feasible; we claim only that it is big enough to 
write a large class of programs efficiently and that it represents a 
reasonable tradeoff of power and simplicity.

Peter

Re: [Spark] Arrays of Strings

[Robert A Duff]

"John R. Strohm" <strohm@airmail.net> writes:

> "Testing cannot be used to show the absence of errors, only their
> resence."  --Edsger W. Dijkstra
 ^
 p

True, but this fact does not imply that so-called "proof of correctness"
can show the absence of errors.  In fact, it cannot.

- Bob

Re: [Spark] Arrays of Strings

[Robert A Duff]

Hyman Rosen <hyrosen@mail.com> writes:

> Matthew Heaney wrote:
> > Doesn't Spark have a #hide clause, to turn off Spark checking?  After
> > all, you're calling a C library function, so what difference does
> > Spark make?
> 
> Getting rid of features that are presumed to cause problems is a bit of
> hubris that language designers always seem to fall victim to. 

As one of the designers of Ada 95, I must say I wholeheartedly agree
with the sentiment here.  Language designers ought to make it easy to
write good programs, not try to make it hard to write bad programs.  Ada
is guilty of the latter in some cases.

However, I think you're being unfair to SPARK here.  SPARK does not say
"you can't do X".  It says, "If you don't do X, then we can prove some
useful properties of your program.  But if you need to do X, then you
can isolate that code, and apply #hide".  That doesn't strike me as
hubris; they're offering you a benefit, in those cases where you can
abide by some restrictions.  You hope that the vast majority of your
code can naturally abide by the restrictions, and isolate the rest in
small packages.

Rod Chapman said it well in another post:

>  The trick with bindings like this is to come up with a package
> specification which is pure SPARK, ...

Non-spark Ada does the same thing in many cases.  Ada does not say, "you
can't do bit-wise type conversions".  Instead it says, "if you want to
do bit-wise conversions, you have to say 'Unchecked_Conversion'".  That
doesn't seem like a restriction to me.  It seems liberating.  It allows
me to have some confidence that the code I'm reading obeys the type
model, so long as I don't see Unchecked_Conversion (or address clauses,
or...).

Contrast with C, where perfectly safe conversions use the same syntax as
potentially troublesome unsafe ones.

My point is:  The language designer should not say "you can't do X"
(assuming X is sometimes useful).  But it's perfectly reasonable for the
language designer to say "if you're going to do X, then you have to say
so".

Back to Hyman:

>...Ada itself
> had a huge problem because the designers thought that function pointers
> could be eliminated.

Agreed.  And C has a huge problem because nested functions are not
allowed.  And both languages (C and Ada) have a huge problem because you
can't pass [pointers to] nested procedures as parameters.

>... Spark gets rid of all pointers, Java gets rid of
> templates, and so on and so on.

I'm not sure Java's lack of templates/generics is due to hubris.
More likely, it's due to trying to [over]simplify the language.

> Then everyone who uses these languages has to figure out how to work
> around the lack of the feature they need, essentially duplicating it in
> some kludgy way. Meanwhile the language designers have their heads in the
> sand and their noses in the air while they pat themselves on the back (:-)
> in self-congratulation on how they have created perfection.

Agreed.

- Bob

Re: [Spark] Arrays of Strings

[Hyman Rosen]

Robert A Duff wrote:
> However, I think you're being unfair to SPARK here.

I'm willing to accept that. As I say here frequently, I don't know Ada,
much less subsets thereof (although I did once work with VHDL). I was
reacting to the OP's code. I agree with the principle that Spark is what
it is, and that non-Spark code should be segregated away into hidden
modules that do what they need to. That's much more reasonable than
trying to express the inexpressible in Spark itself.

Whether or not it's reasonable to program in a language without pointers
is another matter, but I guess if people are happy, more power to them.
I suspect that a lot of Spark code may wind up using arrays and indexes,
just like Fortran.

Re: [Spark] Arrays of Strings

[Lutz Donnerhacke]

* Hyman Rosen wrote:
> Whether or not it's reasonable to program in a language without pointers
> is another matter, but I guess if people are happy, more power to them.
> I suspect that a lot of Spark code may wind up using arrays and indexes,
> just like Fortran.

In order to clarify this and finish my part in this discussion, I prefer the
Spark way of programming for two reasons. First I learned, that the failing
proofs point me directly to logical errors in my program, which are
otherwise hard to find, because I can't trigger them (but my users will). So
developing programs with those constraints results in much more stable
programs for me. Second the prohibition of dynamic storage (including
recursion) urges me to look for more efficient algorithms with bounded space
constraints. Due to the fact I'm playing with embedded (or long life)
systems, my code written is Spark is better adopted to my problems than Ada
code.

Of course, there are several points, I'd like to change. Especially user
constraint types (in order to represent dependent types as a single one)
would be fine.

But back to the topic: Rod's idea is right, but does not go far enough. It
requires a dynamically allocated array of pointers or an error message from
the syscall wrapper. Therefore I seperated this part further and use a user
provided space for this purpose.