[ Jocelyn Ireson-Paine's Home Page | Free software | Publications | Example of Web specification | Report on Visit to University of Minho, May 2000 ]
This page contains the gist of a talk I gave to the University of Minho Informatics Department on algebraic Web specification: using algebraic specification languages, and particularly the compositional power of their module systems, to specify and build Web sites. An example, which you can run in CafeOBJ, is here.
Algebraic Web Specification (AWS): means using an algebraic specification language, i.e. a language whose models are algebras. An algebra is just a mathematical system such as a group, ring, or monoid, with some basic types ('sorts') and some operations on these sorts. Mappings between algebras will usually be important.
Syntax:
module SIMPLE-NAT { [ Zero NzNat < Nat ] --- Sorts (types). --- < denotes subsorting. op 0 : -> Zero --- 0 is an arbitrary constant --- of sort Zero. op s : Nat -> NzNat --- s is a prefix operation from --- Nat to NzNat. op _+_ : Nat Nat -> Nat --- + is an infix operation from Nat Nat to Nat. vars N N' : Nat --- Variables for use in the --- equations. eq 0 + N : = N . --- First equation. eq s(N) + N' = s(N + N') . }
Operational Semantics:
Is via term-rewriting. You can use CafeOBJ much
as a functional programming language, without needing to appreciate the
mathematical foundations (though it helps).
Denotational Semantics:
+-------------------------+ \ Zero | 0, =0+0, =0+0+0, ... | | +-------------------------+ | NzNat | s(0), =0+s(0), ... | > Nat | s(s(0)), =... | | | ... | | +-------------------------+ /
popx@lmf talk]$ cafeobj Loading /usr/local/acl5/libacl503.so. Mapping /usr/local/cafeobj-1.4/bin/cafeobj.acl...done. Mapping /usr/local/acl5/acl503.epll. -- loading standard prelude ; Loading /usr/local/cafeobj-1.4/prelude/std.bin -- CafeOBJ system Version 1.4.3(PigNose.0.935) -- built: 2000 Feb 1 Tue 6:36:56 GMT prelude file: std.bin *** 2000 May 23 Tue 19:15:29 GMT Type ? for help --- built on Allegro CL Trial Edition 5.0 [Linux/X86] (8/29/98 10:57) CafeOBJ> input SIMPLE-NAT.OBJ processing input : /home/popx/talk/SIMPLE-NAT.OBJ -- defining module SIMPLE-NAT....._..* done. CafeOBJ> open SIMPLE-NAT -- opening module SIMPLE-NAT.. done. %SIMPLE-NAT> show . module SIMPLE-NAT { ** opening imports { protecting (BOOL) } signature { [ Nat, Zero NzNat < Nat, NzNat, NzNat < Nat, Zero, Zero < Nat ] op 0 : -> Zero { prec: 0 } op s : Nat -> NzNat { prec: 0 } op _ + _ : Nat Nat -> Nat { strat: (1 0 2) prec: 41 } } axioms { var N : Nat var N' : Nat eq 0 + N = N . eq s(N) + N' = s(N + N') . } } %SIMPLE-NAT> reduce s(s(0)) + s(s(s(0))) . -- reduce in %SIMPLE-NAT : s(s(0)) + s(s(s(0))) s(s(s(s(s(0))))) : NzNat (0.000 sec for parse, 3 rewrites(0.000 sec), 5 matches) %SIMPLE-NAT> quit [Leaving CafeOBJ] ; Exiting Lisp [popx@lmf talk]$ exitNote that in this run, I input
SIMPLE-NAT.OBJ
. The file
with a name that's the same but lower-case, simple-nat.obj
, is
an example which comes with the package. 1,2,3,5 to 50
by 5
.
An example with CafeOBJ. Using the SIMPLE-NAT module, we want to show that 0 is a right identity of + also. Use structural induction to show: 0+0=0; if M+0=M, s(M)+0=s(M). Do the second by introducing a and asserting a+0=a, then reducing s(a)+0.
cafeobj [popx@lmf talk]$ cafeobj Loading /usr/local/acl5/libacl503.so. Mapping /usr/local/cafeobj-1.4/bin/cafeobj.acl...done. Mapping /usr/local/acl5/acl503.epll. -- loading standard prelude ; Loading /usr/local/cafeobj-1.4/prelude/std.bin -- CafeOBJ system Version 1.4.3(PigNose.0.935) -- built: 2000 Feb 1 Tue 6:36:56 GMT prelude file: std.bin *** 2000 May 23 Tue 19:46:48 GMT Type ? for help --- built on Allegro CL Trial Edition 5.0 [Linux/X86] (8/29/98 10:57) CafeOBJ> input SIMPLE-NAT.OBJ processing input : /home/popx/talk/SIMPLE-NAT.OBJ -- defining module SIMPLE-NAT....._..* done. CafeOBJ> open SIMPLE-NAT -- opening module SIMPLE-NAT.. done. %SIMPLE-NAT> op a : -> Nat . %SIMPLE-NAT> eq a + 0 = a . _ %SIMPLE-NAT> reduce 0 + 0 . -- reduce in %SIMPLE-NAT : 0 + 0 0 : Zero (0.000 sec for parse, 1 rewrites(0.000 sec), 2 matches) %SIMPLE-NAT> reduce s(a) + 0 . -- reduce in %SIMPLE-NAT : s(a) + 0 s(a) : NzNat (0.000 sec for parse, 2 rewrites(0.000 sec), 4 matches) %SIMPLE-NAT> close CafeOBJ> quit [Leaving CafeOBJ] ; Exiting LispOther more advanced proof techniques exist. Would be nice to prove properties e.g. that all variants of an input form send the same attributes to the server.
22nd May 2000.
[ Jocelyn Ireson-Paine's Home Page | Free software | Publications | Example of Web specification | Report on Visit to University of Minho, May 2000 ]