Programatica Tools

Demo on April 29, 2003

The Alfa Certificate Server

The purpose of this demo was to show the complete story on how to create an Alfa certificate with the Programatica tools (pfe/pfebrowser) in their current state.

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 .
(One could also have used pfe new *.hs.)
NameLast modifiedSize
Parent Directory  -
Prelude.hs2003-04-29 22:39 6.2K
PreludeList.hs2003-04-29 22:39 1.7K
PreludeText.hs2003-04-29 22:39 546
SPS.hs2003-04-29 23:39 1.5K
SPSProofs.alfa2003-04-30 01:25 2.9K
alfa/2004-11-22 23:29 -
new/2004-11-24 01:48 -
We then started pfebrowser and took a look at the Haskell code for module SPS, noting in particular the following definitions,

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.


Links:
Thomas Hallgren