Institutt for Informatikk (IfI), Universitetet i Oslo

ABEL prosjektet

Prosjektet tar sikte på å videreutvikle språk, metoder, teknikker samt tilhørende teori for programmering, formell spesifikasjon, utvikling av programmer fra spesifikasjoner, samt formell resonnering omkring spesifikasjoner, programmer og sammenhenger mellom disse.

Prosjektet er basert på et eget språk, kalt ABEL (Abstraction Building, Experimental Language), samt underliggende formell logikk. Det arbeides med implementasjon av et «ABEL-system» implementert i Standard ML. Systemet inneholder syntaktisk og semantisk analyse, samt omskrivningsmaskin og et semi-automatisk besvissystem.

For de som har konto her på instituttet ligger et kjørbart system på /hom/prover/bin/abel.

Prosjektmedarbeidere

Ole-Johan Dahl (prof.)
Olaf Owe (prof.)
Tore Bastiasen (stip.)
Olav Andree Brevik (stud., ferdig 1998)
Leif John Korshavn (stud., ferdig 1998)
Arve Hetland (stud.)
Steinar Midtskogen (stud., ferdig 1999)
Jo Harald Totland (stud.)
Martin Thornquist (stud., ferdig 2002)

Dokumentasjon

Innføring

Ny innføring i bevis-systemet for IN217 studenter (31 sider, pdf)
Kort innføring i bevis-systemet for IN217 studenter fra 1998 (11 sider, ps)
Innføring i hele systemet (html).

Kildekode

Dokumentasjon av kildekoden til systemet er laget ved hjelp av ML-Doc.

Hovedfagsoppgaver

Tore Bastiansen: Modulsammensetning og semantisk analyse i ABEL
Olav Andree Brevik: Bevissytem i ABEL: En interaktiv bevishjelper
Leif John Korshavn: Termomskrivningsregler i ABEL: Viktige egenskaper ved omskrivingssystemer
Steinar Midtskogen: Termomskrivingsmaskin i ABEL: anvendt omskrivingsteori og AC-omskriving
Martin Thornquist: An Evaluation of the ABEL System

Artikler

Ole-Johan Dahl and Olaf Owe: Formal Development with ABEL; in LNCS 552 (VDM'91), revised version 1992.
Ole-Johan Dahl, Olaf Owe og Tore Bastiansen: Subtyping and Constructive Specification; Nordic Journal of Computing, 5 (1998)
Bjørn Kristoffersen og Ole-Johan Dahl: On Introducing Higher Order Functions in ABEL; Nordic Journal of Computing
Tore Bastiansen: Parametric subtypes in ABEL; research report 207 (revised version), October 1995.
Ole-Johan Dahl and Bjørn Kristoffersen: On introducing higher order functions in ABEL; research report 210, December 1995. To appear in NJC.
Ole-Johan Dahl and Olaf Owe: On the use of subtypes in ABEL; research report 206 (revised version), October 1995.
Olaf Owe: Partial Logic; Formal aspects of Computing Journal, 1993 (5): 208-223.

Annet

Ole-Johan Dahl: Verifiable Programming, Prentice Hall, (270 pages); 1992
Ole-Johan Dahl, Dag F. Langmyr and Olaf Owe: Preliminary Report on the Specification Language Abel; research report 106, December 1987.

Sist oppdatert: 18. februar 2000