ANN: New technical paper from Ada Europe 2004 now available

ANN: New technical paper from Ada Europe 2004 now available

[Rod Chapman]

I'm pleased to announce the availability of two new technical
papers that were recently presented at Ada Europe 2004.

Both are available now in PDF at www.sparkada.com

Note that the first of these joinly took the best paper award at the
conference.  The latter was awarded best presentation.

"High-Integrity Ada in a UML and C World", Peter Amey and Neil White

Abstract
The dictates of fashion and the desire to use "hot" technology not
only affects software developers but also influences potential
customers. Where once a client was just content to accept something
that worked (actually, would be delighted to have something that
worked) now they are concerned about the means by which it was
constructed; not just in the sense of was it well-enough constructed
but in the more malign sense of was fashionable technology used. This
paper shows how the customer's desire to use de facto standards such
as UML and their wish to use language such as C?perhaps to support a
small or unusual processor; to integrate with other subsystems; for
the perceived comfort of future portability; ot for other,
non-technical reasons?can be aligned with the professional engineer's
need to use those tools and languages which are truly appropriate for
rigorous software development.


"High-Integrity Interfacing to Programmable Logic with Ada"
Adrian J Hilton, Praxis Critical Systems Limited and
Jon G Hall, Open University.

Abstract
Programmable Logic Devices (PLDs) are now common components of
safety-critical systems, and are increasingly used for safety-related
or safety-critical functionality. Recent safety standards demand
similar rigour in PLD specification, design and verification to that
in critical software design. Existing PLD development tools and
techniques are inadequate for the higher integrity levels. In this
paper we examine the use of Ada as a design language for PLDs. We
analyse earlier work on Ada-to-HDL compilation and identify where it
could be improved. We show how program fragments written in the SPARK
Ada subset can be efficiently and rigorously translated into PLD
programs, and how a SPARK Ada program can be effectively interfaced to
a PLD program. The techniques discussed are then applied to a
substantial case study and some preliminary conclusions are drawn from
the results.

Re: ANN: New technical paper from Ada Europe 2004 now available

[Hyman Rosen]

Rod Chapman wrote:
> "High-Integrity Ada in a UML and C World", Peter Amey and Neil White

The automatically generated C in this paper contains

     typedef Colour_ADT_RGB_Value Colour_ADT_Colour[3];
     void Colour_ADT_SWAP(Colour_ADT_Colour *A, Colour_ADT_Colour *B)
     {
         Colour_ADT_Colour Temp;
         memmove((void*)Temp,(void*)A,6);
         memmove((void*)A,(void*)B,6);
         memmove((void*)B,(void*)Temp,6);
     }

Those memmoves exhibit bad C style.

First of all, the casts to void * are unnecessary; in C any pointer
converts automatically to void * and no cast is needed.

Second, coding an explicit 6 for the memmove size is bad practice.
It would make the code unportable to funny architectures such as
some DSPs where the compiler has sizeof(int) = 1.

Third, memmove guarantees that copies of overlapping objects work;
for this case, the more efficient memcpy is better, because there is
no possibility of overlap.

Fourth, the parameters are pointers to arrays, so it's more coherent
stylistically to pass &Temp to the copy function rather than plain
Temp, even though the effect is the same.

It would be much nicer for the code to read

     memcpy(&Temp, A, sizeof(Colour_ADT_Colour));
     memcpy(A, B, sizeof(Colour_ADT_Colour));
     memcpy(B, &Temp, sizeof(Colour_ADT_Colour));

Re: ANN: New technical paper from Ada Europe 2004 now available

[Mike Silva]

Hyman Rosen <hyrosen@mail.com> wrote in message news:<1088612188.693737@master.nyc.kbcfp.com>...
> Rod Chapman wrote:
> > "High-Integrity Ada in a UML and C World", Peter Amey and Neil White
> 
> The automatically generated C in this paper contains
> 
>      typedef Colour_ADT_RGB_Value Colour_ADT_Colour[3];
>      void Colour_ADT_SWAP(Colour_ADT_Colour *A, Colour_ADT_Colour *B)
>      {
>          Colour_ADT_Colour Temp;
>          memmove((void*)Temp,(void*)A,6);
>          memmove((void*)A,(void*)B,6);
>          memmove((void*)B,(void*)Temp,6);
>      }
> 
> Those memmoves exhibit bad C style.

Isn't it really straining to complain about the style (not
correctness, but style) of automatically generated code?  It's just an
intermediate step from the source to the binary, which in this case
happens to be human-readable in order to use a particular set of
tools.  BTW, you didn't point out that Colour_ADT_Colour is never
defined.  That would have been a better criticism! :)

Mike

Re: ANN: New technical paper from Ada Europe 2004 now available

[Hyman Rosen]

Mike Silva wrote:
> Isn't it really straining to complain about the style (not
> correctness, but style) of automatically generated code?

No. One of the claims of the paper is that the generated C
code is readable and maintainable in and of itself; indeed
that is one of the main points of the paper.

>  BTW, you didn't point out that Colour_ADT_Colour is never
> defined.  That would have been a better criticism! :)

I only copied relevant portions, not the entire code.

Re: ANN: New technical paper from Ada Europe 2004 now available

[Peter Amey]

Hyman Rosen wrote:
> Mike Silva wrote:
> 
>> Isn't it really straining to complain about the style (not
>> correctness, but style) of automatically generated code?
> 
> 
> No. One of the claims of the paper is that the generated C
> code is readable and maintainable in and of itself; indeed
> that is one of the main points of the paper.
> 

I don't recall making this claim.  I said that the translation process 
is "transparent and traceable" and that the C provides a useful 
intermediate representation for object code verification purposes.  I 
think these statement stand.

We certainly wouldn't recommend modification of the C because that 
immediately throws away all the verification benefits that have been 
gain by analysing the intermediate SPARK model.

It is probably true that the C /could/ be maintained if, for example, 
the translation or SPARK parts of the tool chain were suddenly to become 
unavailable.

Peter

Re: ANN: New technical paper from Ada Europe 2004 now available

[Hyman Rosen]

Peter Amey wrote:
> I don't recall making this claim.  I said that the translation process 
> is "transparent and traceable" and that the C provides a useful 
> intermediate representation for object code verification purposes.  I 
> think these statement stand.
> 
> We certainly wouldn't recommend modification of the C because that 
> immediately throws away all the verification benefits that have been 
> gain by analysing the intermediate SPARK model.
> 
> It is probably true that the C /could/ be maintained if, for example, 
> the translation or SPARK parts of the tool chain were suddenly to become 
> unavailable.

True. But the paper does talk about generating "deliverable" C,
and clearly that C code is meant to be read, not just compiled.
You wouldn't want your target audience, who are presumably expert
in C and already suspicious of using a different language, to be
able to nitpick the way I just did.

Re: ANN: New technical paper from Ada Europe 2004 now available

[Wes Groleau]

Hyman Rosen wrote:
> and clearly that C code is meant to be read, not just compiled.

C code that's meant to be read?  Surely you jest.

(Just kidding, Hyman, just kidding!  Couldn't resist a little dig.)

-- 
Wes Groleau

People would have more leisure time if it weren't
for all the leisure-time activities that use it up.
                        -- Peg Bracken