Programatica ToolsProgramatica Tools
The starting point for the demo was a Haskell module defining synchronous stream processors, and asserting a simple separation property for parallel composition of synchronous stream processors.
Normally, you would start by creating a PFE project using
pfesetup, but since that would create references to the normal
Haskell 98 Prelude, which the Alfa translator isn't quite good enough to handle
yet, we instead used a stripped down version of the Prelude, copied
from the directory
programatica/tools/hs2alfa/tests
in the Programatica CVS repository. The PFE project was then created in
the following way:
pfe new SPS.hs
pfe chase .
pfe new *.hs.)
| Name | Last modified | Size |
|---|---|---|
| Parent Directory | - | |
| new/ | 2004-11-24 01:48 | - |
| alfa/ | 2004-11-22 23:29 | - |
| SPSProofs.alfa | 2003-04-30 01:25 | 2.9K |
| SPS.hs | 2003-04-29 23:39 | 1.5K |
| PreludeText.hs | 2003-04-29 22:39 | 546 |
| PreludeList.hs | 2003-04-29 22:39 | 1.7K |
| Prelude.hs | 2003-04-29 22:39 | 6.2K |
| S i o | the synchronous stream processor type |
| runS | the function that applies a stream processor to an input stream
to produce an output stream,
S i o -> [i] -> [o]
|
| >*< | Parallel composition of stream processors,
S i1 o1 -> S i2 o2 -> S (i1, i2) (o1, o2)
|
| Separation1 | The asserted separation property, for which we wanted to create an Alfa
certificate:
{runS (sps1>*<sps2) (zip is1 is2)} === {zip (runS sps1 is1) (runS sps2 is2)} |
The source code already contained the certificate annotation
{-#cert:Seperation1#-} next to the assertion,
telling pfebrowser to display a certificate icon there.
The icon displayed initially was a sad smiley, indicating that pfebrowser
did not find a certificate of the name given in the certificate annotation.
Our first step was to create the Alfa certificate. This was done by clicking on the assertion name (Separation1), then on the link Create a new certificate that appeared in the status display below the source display in the pfebrowser window. Pfebrowser then opened a window, where the type, name and conclusion of the new certificate could be entered:
We then obtained a new, unvalidated certificate, and the sad smiley icon next to the assertion changed accordingly. Clicking on that icon opened the certificate info window,
where a link to validate the certificate appeared. Validating the certificate might seem pointless at this point, considering that we haven't created a proof yet. It is still the best way to proceed, because it will have the effect of translating the Haskell code to Alfa and creating a template proof file were we can put our proof.
The tools put the Alfa translation in the subdirectory alfa/, and the proof template file created was called SPSProofs.alfa. (The Alfa certificate server currently suggests one proof file per Haskell module, named module name++"Proofs.alfa". A future version of pfebrowser will provide a way for the user to edit certificate attributes, such as the names of proof files.)
We then proceeded to edit the proof in the proof file, and eventually ended up with a complete proof of the asserted property (in the file SPSProofs.alfa, best viewed in Alfa). We also manually ran the termination checker to verify that the proof was defined by structural induction rather than some meaningless circular construction.
We then clicked on the certificate icon again, and then on the link to validate, and this time the validation succeeded.
