* [Spark] Some Linux tools
@ 2003-03-21 17:07 Lutz Donnerhacke
2003-03-24 14:08 ` Lutz Donnerhacke
0 siblings, 1 reply; 10+ messages in thread
From: Lutz Donnerhacke @ 2003-03-21 17:07 UTC (permalink / raw)
1) If using the standard Spark tools, it's not that refreshing to wait on a
somewhat slower machine for the results ... To have a look is more
interesting.
2) Sometimes the simplifier can not solve all trivial problems. There might
be a very simple hint to guide the simplifier to the right result. But
in order to do so, the *.rls files has to be changed, before the simplifier
can run.
3) In order to provide the examiner access to the necessary sources, a simple
way is using an index file. This should be easily generated.
ftp://ftp.iks-jena.de/pub/mitarb/lutz/ada/spark/ contains two files:
rules.pl replacement of sparksimp working on 1) and 2)
spark_update_index.pl working on 3) (errornous, take with grain)
Have fun.
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Some Linux tools
2003-03-21 17:07 [Spark] Some Linux tools Lutz Donnerhacke
@ 2003-03-24 14:08 ` Lutz Donnerhacke
2003-03-27 18:03 ` Rod Chapman
2003-04-08 13:46 ` Rod Chapman
0 siblings, 2 replies; 10+ messages in thread
From: Lutz Donnerhacke @ 2003-03-24 14:08 UTC (permalink / raw)
* Lutz Donnerhacke wrote:
> 1) If using the standard Spark tools, it's not that refreshing to wait on a
> somewhat slower machine for the results ... To have a look is more
> interesting.
>
> 2) Sometimes the simplifier can not solve all trivial problems. There might
> be a very simple hint to guide the simplifier to the right result. But
> in order to do so, the *.rls files has to be changed, before the simplifier
> can run.
>
> 3) In order to provide the examiner access to the necessary sources, a simple
> way is using an index file. This should be easily generated.
>
> ftp://ftp.iks-jena.de/pub/mitarb/lutz/ada/spark/ contains two files:
> rules.pl replacement of sparksimp working on 1) and 2)
> spark_update_index.pl working on 3) (errornous, take with grain)
I replaced the rules.pl by sparksimp.pl.
Of course, this program does not require 12MB stack space like pogs.
If you need other outputs, please mail me.
$ sparksimp.pl --help
Usage: sparksimp.pl [rulefile]
Searches for all unsimplified 'vcg' files, modifies the 'rls' file, if
necessary, invokes the simplifier, and generate a pogs like statistics report.
The rulefile may consists of additional rules for examiner generated rule
families. Every rule set starts with a comma seperated list of target families
followed by the space indented rules themself. The following example was the
reason to introduce this feature:
kill_group_rules, kill_all_rules:
- X <= Y may_be_replaced_by X >= - Y.
- X >= Y may_be_replaced_by X <= - Y.
$ sparksimp.pl kernel.rul
Switching to .
Adding directory kernel_
Switching to kernel_
Adding directory io
Adding directory processes
Switching to io
permission_to_string: Testing ... reading ... simplifying
[A two line progess indicator is shown here:
First line: procedure/function currently simplified with proof counter.
Second line: Last line of the spadesimp stdout log.]
permission_to_string: Collecting statistics ... vcg, siv ... done
mode_to_string: Testing ... reading ... simplifying
mode_to_string: Collecting statistics ... vcg, siv ... done
string_to_fullpath: Testing ... reading ... simplifying
string_to_fullpath: Collecting statistics ... vcg, siv ... done
mkdir: Testing ... reading ... simplifying
mkdir: Collecting statistics ... vcg, siv ... done
rename: Testing ... reading ... simplifying
rename: Collecting statistics ... vcg, siv ... done
getdents_empty: Testing ... reading ... simplifying
getdents_read: Collecting statistics ... vcg, siv ... done
getdents: Testing ... reading ... simplifying
getdents: Collecting statistics ... vcg, siv ... done
Switching back
Switching to processes
kill_all: Testing ... done
kill_all: Collecting statistics ... vcg, siv ... done
kill_process: Testing ... done
kill_process: Collecting statistics ... vcg, siv ... done
kill_my_group: Testing ... done
kill_my_group: Collecting statistics ... vcg, siv ... done
kill_group: Testing ... done
kill_group: Collecting statistics ... vcg, siv ... done
Switching back
Switching back
Writing statistics ... done
$ cat kernel.sum
-------------------------------------------------------------------------------
Semantic Analysis Summary
-------------------------------------------------------------------------------
Summary of:
Verification Condition files (.vcg)
Simplified Verification Condition files (.siv)
in the directory: /var/home/lutz/work/ada/src/kernel
VCs for kernel_/processes/kill_process
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 26 | YES |
2 | start | rtc check @ 26 | YES |
3 | start | rtc check @ 26 | YES |
4 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/getdents
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 140 | YES |
2 | start | rtc check @ 141 | YES |
3 | start | rtc check @ 143 | YES |
4 | start | rtc check @ 145 | YES |
5 | start | finish | YES |
6 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/mode_to_string
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 60 | YES |
2 | start | rtc check @ 67 | YES |
3 | start | rtc check @ 68 | YES |
4 | start | assert @ 71 | YES |
5 | start | assert @ 71 | YES |
6 | start | assert @ 71 | YES |
7 | assert @ 71 | rtc check @ 73 | YES |
8 | assert @ 71 | rtc check @ 74 | YES |
9 | assert @ 71 | assert @ 77 | YES |
10 | assert @ 71 | assert @ 77 | YES |
11 | assert @ 71 | assert @ 77 | YES |
12 | assert @ 77 | rtc check @ 79 | YES |
13 | assert @ 77 | rtc check @ 80 | YES |
14 | assert @ 77 | assert @ 83 | YES |
15 | assert @ 77 | assert @ 83 | YES |
16 | assert @ 77 | assert @ 83 | YES |
17 | assert @ 83 | rtc check @ 85 | YES |
18 | assert @ 83 | rtc check @ 86 | YES |
19 | assert @ 83 | rtc check @ 87 | YES |
20 | assert @ 83 | rtc check @ 88 | YES |
21 | assert @ 83 | rtc check @ 89 | YES |
22 | assert @ 83 | rtc check @ 90 | YES |
23 | assert @ 83 | rtc check @ 91 | YES |
24 | assert @ 83 | finish | YES |
25 | assert @ 83 | finish | YES |
26 | assert @ 83 | finish | YES |
27 | assert @ 83 | finish | YES |
28 | assert @ 83 | finish | YES |
29 | assert @ 83 | finish | YES |
30 | assert @ 83 | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/processes/kill_my_group
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 33 | YES |
2 | start | rtc check @ 33 | YES |
3 | start | rtc check @ 33 | YES |
4 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/getdents_empty
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/getdents_read
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 185 | YES |
2 | start | rtc check @ 186 | YES |
3 | start | rtc check @ 190 | YES |
4 | start | rtc check @ 191 | YES |
5 | start | rtc check @ 194 | YES |
6 | start | rtc check @ 195 | YES |
7 | start | rtc check @ 196 | YES |
8 | start | rtc check @ 197 | YES |
9 | start | rtc check @ 197 | YES |
10 | start | assert @ 197 | YES |
11 | assert @ 197 | assert @ 197 | YES |
12 | assert @ 197 | rtc check @ 200 | YES |
13 | assert @ 197 | rtc check @ 201 | YES |
14 | start | rtc check @ 208 | YES |
15 | start | rtc check @ 208 | YES |
16 | assert @ 197 | rtc check @ 208 | YES |
17 | assert @ 197 | rtc check @ 208 | YES |
18 | start | finish | YES |
19 | start | finish | YES |
20 | start | finish | YES |
21 | start | finish | YES |
22 | assert @ 197 | finish | YES |
23 | assert @ 197 | finish | YES |
24 | assert @ 197 | finish | YES |
25 | assert @ 197 | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/permission_to_string
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 18 | YES |
2 | start | rtc check @ 19 | YES |
3 | start | rtc check @ 19 | YES |
4 | start | rtc check @ 20 | YES |
5 | start | rtc check @ 20 | YES |
6 | start | rtc check @ 20 | YES |
7 | start | rtc check @ 20 | YES |
8 | start | finish | YES |
9 | start | finish | YES |
10 | start | finish | YES |
11 | start | finish | YES |
12 | start | finish | YES |
13 | start | finish | YES |
14 | start | finish | YES |
15 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/processes/kill_group
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 40 | YES |
2 | start | rtc check @ 41 | YES |
3 | start | rtc check @ 42 | YES |
4 | start | rtc check @ 42 | YES |
5 | start | rtc check @ 42 | YES |
6 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/mkdir
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 241 | YES |
2 | start | rtc check @ 241 | YES |
3 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/string_to_fullpath
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 99 | YES |
2 | start | assert @ 99 | YES |
3 | assert @ 99 | assert @ 99 | YES |
4 | assert @ 99 | rtc check @ 102 | YES |
5 | start | rtc check @ 104 | YES |
6 | assert @ 99 | rtc check @ 104 | YES |
7 | start | finish | YES |
8 | assert @ 99 | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/processes/kill_all
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 20 | YES |
2 | start | rtc check @ 20 | YES |
3 | start | rtc check @ 20 | YES |
4 | start | finish | YES |
-------------------------------------------------------------------------------
\fVCs for kernel_/io/rename
-------------------------------------------------------------------------------
| | |--- Proved In --- |
No | From | To | vcg siv plg prv TODO |
-------------------------------------------------------------------------------
1 | start | rtc check @ 249 | YES |
2 | start | rtc check @ 249 | YES |
3 | start | finish | YES |
-------------------------------------------------------------------------------
\f===============================================================================
--------------- Proved By --------------
Total Examiner Simplifier Checker Review Undischarged
Assert 13 0 13 0 0 0
Postcondition 34 34 0 0 0 0
Runtime check 62 0 62 0 0 0
===============================================================================
Totals 109 34 75 0 0 0
% Totals 31% 68% 0% 0% 0%
===================== End of Semantic Analysis Summary ========================
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Some Linux tools
2003-03-24 14:08 ` Lutz Donnerhacke
@ 2003-03-27 18:03 ` Rod Chapman
2003-03-28 11:47 ` Lutz Donnerhacke
2003-04-08 13:46 ` Rod Chapman
1 sibling, 1 reply; 10+ messages in thread
From: Rod Chapman @ 2003-03-27 18:03 UTC (permalink / raw)
Lutz,
Thanks for posting those scripts - I'm sure many buyers of the SPARK
book will find them useful. Can you clarify two issues, though:
1) Who is the copyright holder for these scripts?
2) Under what licence terms are these scripts supplied?
Thanks,
Rod
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Some Linux tools
2003-03-27 18:03 ` Rod Chapman
@ 2003-03-28 11:47 ` Lutz Donnerhacke
2003-03-28 15:27 ` Lutz Donnerhacke
2003-03-31 17:25 ` Stephen Leake
0 siblings, 2 replies; 10+ messages in thread
From: Lutz Donnerhacke @ 2003-03-28 11:47 UTC (permalink / raw)
* Rod Chapman wrote:
> Thanks for posting those scripts - I'm sure many buyers of the SPARK
> book will find them useful. Can you clarify two issues, though:
> 1) Who is the copyright holder for these scripts?
Lutz Donnerhacke, Jena, Thuringia, Germany, Europe, Earth, Solar System,
Milky Way, Local Group, ...
> 2) Under what licence terms are these scripts supplied?
Free licence: Take it at your own risk, modify it, keep the modifications
secret, sell them, ignore to mention me, ...
If someone provide me an example output of the Proof Checker logfile, I can
add this. Path functions are unsupported, because I do not need them.
(Larger programs are usually GP(L)Led.)
Recent modifications:
- Computes hashs over VCs in order to check them against those mentioned in
the Review Team logfile. This ensures, that modified VCs are not longer
considered proofed by the review team.
- Prints 'old' instead of 'yes' in the summary if the simplifier/checker
result is older than the examiner output.
In order to considerably speed up the simplifier/checker process, it's worth
to check hashs over the examiner generated files. This may render several
simplifier/checker calls unnecessary due to unmodified preconditions.
I'll think about this.
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Some Linux tools
2003-03-28 11:47 ` Lutz Donnerhacke
@ 2003-03-28 15:27 ` Lutz Donnerhacke
2003-03-31 17:25 ` Stephen Leake
1 sibling, 0 replies; 10+ messages in thread
From: Lutz Donnerhacke @ 2003-03-28 15:27 UTC (permalink / raw)
* Lutz Donnerhacke wrote:
> In order to considerably speed up the simplifier/checker process, it's worth
> to check hashs over the examiner generated files. This may render several
> simplifier/checker calls unnecessary due to unmodified preconditions.
Done.
sparksimp.pl now uses a *.hash file containing the hash over *.{vcg,fdl,rls}
in order to check if the simplifier has to be run or if touching the *.siv
file is equivalent.
If you do not logically modify a function, the simplifier will not be run
for this function, even if you modify other functions in the same file.
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Some Linux tools
2003-03-28 11:47 ` Lutz Donnerhacke
2003-03-28 15:27 ` Lutz Donnerhacke
@ 2003-03-31 17:25 ` Stephen Leake
2003-04-01 8:14 ` Lutz Donnerhacke
2003-04-01 8:38 ` Jacob Sparre Andersen
1 sibling, 2 replies; 10+ messages in thread
From: Stephen Leake @ 2003-03-31 17:25 UTC (permalink / raw)
Lutz Donnerhacke <lutz@iks-jena.de> writes:
> * Rod Chapman wrote:
> > Thanks for posting those scripts - I'm sure many buyers of the SPARK
> > book will find them useful. Can you clarify two issues, though:
> > 1) Who is the copyright holder for these scripts?
>
> Lutz Donnerhacke, Jena, Thuringia, Germany, Europe, Earth, Solar System,
> Milky Way, Local Group, ...
>
> > 2) Under what licence terms are these scripts supplied?
>
> Free licence: Take it at your own risk, modify it, keep the modifications
> secret, sell them, ignore to mention me, ...
I think the best way to state that license is "Public Domain".
--
-- Stephe
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Some Linux tools
2003-03-31 17:25 ` Stephen Leake
@ 2003-04-01 8:14 ` Lutz Donnerhacke
2003-04-01 8:38 ` Jacob Sparre Andersen
1 sibling, 0 replies; 10+ messages in thread
From: Lutz Donnerhacke @ 2003-04-01 8:14 UTC (permalink / raw)
* Stephen Leake wrote:
> Lutz Donnerhacke <lutz@iks-jena.de> writes:
>> Free licence: Take it at your own risk, modify it, keep the modifications
>> secret, sell them, ignore to mention me, ...
>
> I think the best way to state that license is "Public Domain".
Possibly, I'm not familiar with software licencing.
BTW: I added separate subunit support to those tools, because I reached the
limits of the demo version.
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Some Linux tools
2003-03-31 17:25 ` Stephen Leake
2003-04-01 8:14 ` Lutz Donnerhacke
@ 2003-04-01 8:38 ` Jacob Sparre Andersen
2003-04-01 9:18 ` Adrian Knoth
1 sibling, 1 reply; 10+ messages in thread
From: Jacob Sparre Andersen @ 2003-04-01 8:38 UTC (permalink / raw)
Stephen Leake wrote:
> Lutz Donnerhacke <lutz@iks-jena.de> writes:
>>Free licence: Take it at your own risk, modify it, keep the modifications
>>secret, sell them, ignore to mention me, ...
>
> I think the best way to state that license is "Public Domain".
It might be, if Lutz was located in USA, but in EU there is legally no
such thing as "public domain".
Greetings,
Jacob (who is a physicist, not a lawyer)
--
"simply because no one had discovered a cure for the universe as a
whole - or rather the only one that did exist had been abolished"
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Some Linux tools
2003-04-01 8:38 ` Jacob Sparre Andersen
@ 2003-04-01 9:18 ` Adrian Knoth
0 siblings, 0 replies; 10+ messages in thread
From: Adrian Knoth @ 2003-04-01 9:18 UTC (permalink / raw)
Jacob Sparre Andersen <sparre@crs4.it> wrote:
>>>Free licence: Take it at your own risk, modify it, keep the modifications
>>>secret, sell them, ignore to mention me, ...
>> I think the best way to state that license is "Public Domain".
> It might be, if Lutz was located in USA, but in EU there is legally no
> such thing as "public domain".
Call it BSD-license. It's like "take it and do what you want with it".
Microsoft did so with the IP-stack in Windows (I guess it's from 4.4BSD)
The GPL which is mainly used in GNU-environments (FSF, Linux and its
userland) is more restrictive.
At least the copyright in Germany is always assigned to the author,
it cannot be given away. Of course there are parts of your rights
you may sell (or not), but this is more like "licensing a product",
to permit use or copying, but the owner is forever the author.
Some years (approx. 80) after the author's dead the rights will expire
and the product/invention becomes a public good. This question always
raises when performing music. For actual music you have to pay a fee
to GEMA, but if the componist is long enough buried five feet under
sealevel then public presentation of his songs is legal without payment.
--
mail: adi@thur.de http://adi.thur.de PGP: v2-key via keyserver
Liebe deinen n�chsten so wie den ersten!
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [Spark] Some Linux tools
2003-03-24 14:08 ` Lutz Donnerhacke
2003-03-27 18:03 ` Rod Chapman
@ 2003-04-08 13:46 ` Rod Chapman
1 sibling, 0 replies; 10+ messages in thread
From: Rod Chapman @ 2003-04-08 13:46 UTC (permalink / raw)
Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:
> Of course, this program does not require 12MB stack space like pogs.
This problem is now corrected in POGS version 3.1 for Linux. POGS
should now run within the default stack size limit of all standard
Linux distributions.
This is now available for download from www.sparkada.com/book.html
- Rod Chapman, SPARK Team
^ permalink raw reply [flat|nested] 10+ messages in thread
end of thread, other threads:[~2003-04-08 13:46 UTC | newest]
Thread overview: 10+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2003-03-21 17:07 [Spark] Some Linux tools Lutz Donnerhacke
2003-03-24 14:08 ` Lutz Donnerhacke
2003-03-27 18:03 ` Rod Chapman
2003-03-28 11:47 ` Lutz Donnerhacke
2003-03-28 15:27 ` Lutz Donnerhacke
2003-03-31 17:25 ` Stephen Leake
2003-04-01 8:14 ` Lutz Donnerhacke
2003-04-01 8:38 ` Jacob Sparre Andersen
2003-04-01 9:18 ` Adrian Knoth
2003-04-08 13:46 ` Rod Chapman
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox