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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,77b4bef87595d604
X-Google-Attributes: gid103376,public,usenet
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news1.google.com!news4.google.com!feeder3.cambrium.nl!feeder1.cambrium.nl!feed.tweaknews.nl!not-for-mail
From: Ludovic Brenta <ludovic@ludovic-brenta.org>
Newsgroups: comp.lang.ada
Subject: Re: Test tool not only for Ada
References: <fnapeb$5ra$1@tamarack.fernuni-hagen.de>
Date: Thu, 24 Jan 2008 22:20:51 +0100
Message-ID: <87myqux6mk.fsf@ludovic-brenta.org>
User-Agent: Gnus/5.110006 (No Gnus v0.6) Emacs/21.4 (gnu/linux)
Cancel-Lock: sha1:DajGmbNd8FcSnYyPECh4iEXEWXw=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Organization: Tele2
X-Trace: 
 DXC=jPZLokTRac=]hSjkKH<@E26`Y6aWje^Y:enDN=EYl4m<6[b\^[?Bi56D@mVgZ>o^?8V?UQ<WJa7g1
Xref: g2news1.google.com comp.lang.ada:19587
Date: 2008-01-24T22:20:51+01:00
List-Id: <comp.lang.ada>

"S�nke Brix" writes:
> Hi Softwareengineers and Testgurus,
>
> 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?
>
> So, who has a deep knowledge and is able to explain the secrets of this test
> tool and especially the mathematics and techniques behind the scenes.
>
> Thanx

I think you should qsk them for the details.  I attended their
presentation at the Ada-Belgium general assembly in 2003 [1].  The
basic principle is to leverage the rich information contained in a
typical Ada program, especially the range constraints, and then
propagating these constraints down every execution path to detect
possible violations.  This analysis is only possible in Ada; lesser
languages require annotations to provide the information about range
constraints.

[1] http://www.cs.kuleuven.be/~dirk/ada-belgium/events/03/030225-abga-event.html

-- 
Ludovic Brenta.