[ Jocelyn Paine's Home Page | Free software | Publications | Example of Web specification | Report on Visit to University of Minho, May 2000 ]

Algebraic Web specification: talk given on Wednesday May 24th

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.

Introduction. I shall talk about using algebraic specification to specify and build Web sites.
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.
My motivation for AWS.
- Automatic documentation generation. I was Invited to work on a credit-scoring project for banks. Many different users for the scoring programs, some needed to know more about these than others. Nice to customise documentation to individual users' needs. Traditionally, this would be done by using an extended HTML, e.g. Java Server Pages (JSP), with conditionals in each page testing the user's level. But nice to have a more global spec: "advanced users need P2, P3, P5; basic users need P4, P5 (not regressions), P7, glossary". Note that nowdays, we might do it with special XML markup and parsers.
- Generating different reading orders. E.g. a photo gallery where photos could be viewed in order of time taken or of place or of (e.g.) style of costume.
- The knowledge that I have a powerful specification language, with a module composition system that makes it easy to combine and parameterise modules, and to get different views of modules.

CafeOBJ is the specification language. Developed by a consortium led by Kokichi Futatsugi, latest in the OBJ line of development which started in the 80s.

An example module.

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)), =...           |   |
        | ...                     |   |
        +-------------------------+   /

An example run:

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]$ exit

Note 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.

To use CafeOBJ here: I have installed it on LMF, and downloaded the package you need to install on other Linuxes. See my report on this visit. Zé Bernardo Barros has copies of the manual and CafeOBJ report (book by Diaconescu and Futatsugi specifying the semantics).
Particular advantages of CafeOBJ for AWS.
- The module system ('programming in the large'/'hyperprogramming' - phrases coined by Goguen). Easy to write parameterisable specs and plug in, e.g. different servers with their own document root, filename conventions etc.
- Clear semantics, with close connection to logic.
- But researchers rarely use the best tool, but the tool that they grew up with/their professor had/they could find on the Web/was free. There may be other languages of equal value - I like CafeOBJ, but the main point of the talk is AWS, not the spec language.
Other possible uses for AWS.
- Defining specific kinds of site, e.g. slideshows with next/back buttons. An example.
- Templates for sites, to ensure consistent headers and footers. Most Web tools use server-side include or (even more) ad-hoc methods. (Slideshows also need consistent headers
- In general, ease of constructing repetitive parts of sites. An example - each large photo is generated from the small in the same way.
- Input forms. E.g. the menus in our Virtual Economy. HTML menu notation is verbose; we'd like something simpler, e.g. 1,2,3,5 to 50 by 5.
- Verified links. "This link here must point to information about CafeOBJ".
Maintainability. With a slideshow written in HTML, one must inspect every page in order to discover that there's a linear reading order. It would be good to have this information more directly available from the Web site spec.

Automatic proof. Any specification language should be easier to prove properties by pencil and paper than e.g. an imperative language like Java. Some languages also have (semi-)automatic proof tools.

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 Lisp

Other 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.

My demonstration is here. This is not at all the full range of things I hope we can do with AWS, indeed, it's little more than using CafeOBJ as a functional programming language.

22nd May 2000.

[ Jocelyn Paine's Home Page | Free software | Publications | Example of Web specification | Report on Visit to University of Minho, May 2000 ]