"S�nke Brix" <soenke.brix@fernuni-hagen.de> wrote in message 
news:fnapeb$5ra$1@tamarack.fernuni-hagen.de...
>
> I read something about the tool "PolySpace". The test approach of this 
> tool
> seems a little bit different. In an advertisment the company describes 
> that
> "PolySpace"
> - ...statically analyses the dynamics of sw applications by relying solely
> on the source code,
> - ...no test cases to write
> - ...no instrumentation of the code
> - ...no execution of the application
> Hmmm ????
> How does this stuff work? I found some infos, but they were not very
> helpful. Something over "semantic analysis", but not very deep. I this a
> pure mathematically analysis scheme?

The general technique used is called 'Abstract Interpretation'.  By 
modelling the semantics of a program and knowing the possible values of the 
variables at one point in the program, the values at another point can be 
determined.

For instance given an integer 'x' which might have the values 1..20, and the 
statement:
    y := x *2;

We can determine the set of values of 'y'.  By following the computations 
through in this manner it is possible to determine whether, at any point, a 
constraint error would arise.  Normally such an event would indicate there 
was an error or deficiency in the program.  Whether the program does what 
you want is another matter - and in this respect I do not think the tool as 
described helps you.  That said, it is often a greater challenge to ensure a 
program is free from defects than check whether it does what you want in 
most circumstances.

The interesting challenge for 'Abstract Interpretation' tools is deciding 
how much detail to preserve at each stage.  From the example should the tool 
note that 'y' might have the values 2..40 or the set of values {2, 4, 6, 
..., 40}.

This can become important, for instance if you had the statement:
   z := 1000 / (y - 9);

Could a divide by zero occur?  If you had a lax model of 'y'  [2..40] you 
would be concerned, but a more accurate model would dispel the concern.  The 
problem with keeping fully accurate models is that the modelling can quickly 
become very complex.  Addressing these issues, to reduce false warnings but 
still give good performance, is a significant matter for these tools. 
 [BTW - on such a simple example the tools would easily determine that a 
divide by zero would not occur].

A similar tool to Polyspace is ASTREE - and there are others.  There is a 
fair deal of information out there on the internet.

Interestingly, with an appropriately designed Ada program much of the 
information needed to enhance code analysis can be derived from the type 
system.  When analysing C programs you typically need a Data Dictionary to 
help manage the analysis effectively [though it is still possible to perform 
useful analyses without one].

Regards
-- 
Stuart