Spark non-working example in book ?

Spark non-working example in book ?

[milouz]

Hi,

I'm learning Spark and I'm currently trying to understand how to prove the 'find_smallest' function describe in chapter 15 (sections 5 and 6).

There are 2 examples in the book.

The one in 15.5 needs the Checker tool. I was expecting to find some *.rul file in the example tarball (found on altran-praxis website), but there's none. 

About the 2nd example, in 15.6, the book is not clear about the need or not of the Checker tool. There's no *.rul nor *.rlu file and the downloaded example don't work either.

Maybe it's normal.... anyway, I'd just like to understand how to prove that the 'find_smallest' function really return the index of the smallest element in an array.

Some clues ?
Regards,

Arnauld

Re: Spark non-working example in book ?

[Phil Thornley]

In article <695e718e-2c5d-4db8-b8e7-d099f4a305db@googlegroups.com>, 
a.michelizza@gmail.com says...
> 
> Hi,
> 
> I'm learning Spark and I'm currently trying to understand how to prove the 'find_smallest' function describe in chapter 15 (sections 5 and 6).
> 
> There are 2 examples in the book.
> 
> The one in 15.5 needs the Checker tool. I was expecting to find some *.rul file in the example tarball (found on altran-praxis website), but there's none. 
> 

This section is now somewhat redundant, particularly for anyone starting 
to learn SPARK and using the current version. (It is perhaps there for 
anyone who used earlier versions, and wants to see something familiar.)

> About the 2nd example, in 15.6, the book is not clear about the need or not of the Checker tool. There's no *.rul nor *.rlu file and the downloaded example don't work either.
> 

No, there is no need to use the Checker - but you do have to use 
Victor/Alt-Ergo to complete all the proofs. How you do this depends on 
how you are using the tools. (If you are using GPS then the switch to 
use Victor isn't set in the provided gpr file - it's on the SPARKSimp 
tab under Switches.)

You also have to provide the 'perm' rule specified at the bottom of page 
442. (Note that the function is called "perm" in the book but is 
"permutation" in the downloaded code, so the rule you need is:
perm(1): permutation(A,C)
           may_be_deduced_from
       [ permutation(A,B),
         permutation(B,C) ] .
Put this in a file called sort.rlu (or array_utilities.rlu) in the 
array_utilities folder.

All the VCs are then proved.

Cheers,

Phil

Re: Spark non-working example in book ?

[milouz]

Thanks, it works great!