🚀 go-pugleaf

From: weigele@prg.oxford.ac.uk
To: mod-ki@unido.uucp
Date: Wed, 1 Nov 89 14:58:56 GMT
Subject: Mathematik der Programmkonstruktion
Keywords: Literatur, Rezensionen

mod-ki message 0325
************************************************************************
Copyright (c) 1989 Martin Weigele Oxford

Das folgende Buch sei allen an Fragen  der  Spezifikation,  Verifikation
und Konstruktion interessierten Lesern von mod-ki empfohlen:

     J. L. A. van den Snepscheut (Ed.):
     Mathematics of Program Construction.
     Springer LNCS 375, 1989.

Der Konferenzband berichtet ueber die gleichnamige Konferenz anlaesslich
des 375. Geburtstages der Universitaet Groningen/NL.

Etwa ein Drittel der Beitraege liegen  den  "invited lectures"  (Abrial,
Chandy, Hehner, May/Sheppard, Meertens, Misra) zugrunde, der  Rest  sind
normale Beitraege.

Die Beitraege stehen in der Tradition  der  Axiomatischen  Spezifikation
(Hoare, Dijkstra) und der darauf aufbauenden mathematischen Theorie  der
Verfeinerung (Back, Morgan).

Insgesamt  ist  das  Bemuehen  deutlich,  eine  allgemeine  Theorie  der
Programmentwicklung   zu   schaffen,   die    Nichtdeterminismus    bzw.
Nebenlaeufigkeit (Concurrency) sowohl auf der  Spezifikationsebene,  als
auch als moegliche Implementierung auf natuerliche  Weise  einschliesst.
In diesem  Zusammenhang  ist  besonders  der  Artikel  von  J. R. Abrial
hervorzuheben,  der  "A  Formal Approach to Large Software Construction"
beschreibt. Weiter werden Action Systems bis hin zu Analogen  Neuronalen
Netzen zu  solcher  Mathematik  der  Programmkonstruktion  in  Beziehung
gesetzt.  Mit  OCCAM  ist  auch  das  Implementierungs"ende"  vertreten.
Bemerkenswert ist der starke Bezug zum  praktischen  Computerexperiment;
trotzdem duerfte das Buch auch den Theoretikern gefallen.

Der    entscheidende    Durchbruch    gegenueber     der     klassischen
Programmverifikation,  wie  sie  auch  in  der   deutschen   KI-Gemeinde
betrieben  wurde,  besteht  darin,  dass  statt   konkreten   Programmen
zunaechst  abstrakte  Programme  in  den  Mittelpunkt  der   Betrachtung
gestellt werden, deren  Eigenschaften  unabhaengig  von  Maschinen  oder
Programmiersprachen betrachtet werden  koennen.  Damit  wird  die  sonst
zwangslaeufige Explosion von Details in  handhabbarere  Bahnen  gelenkt.
Das Vehikel hierzu ist nicht zuletzt Nichtdeterminismus (beschraenkt und
unbeschraenkt).  Im  Grunde  bedeutet  dies  die  konsequente  Umsetzung
traditionellen Software-Engineerings a la Wirth in einen  mathematischen
Rahmen.  Am  Endpunkt  koennte  eine   Verschmelzung   mit   Ideen   des
Automatischen  Beweisens  stehen,  die  vielleicht  die  Abloesung   des
Resolutionsprinzips als zu maschinennah einlaeuten koennte... Dann  gibt
es endlich eine  Rechtfertigung  fuer  unterschwelliges  Unbehagen  beim
Umgang mit Klauselgraphen!

Martin Weigele, z.Zt. PRG, Oxford University Computing Lab.

------------------------------------------------------------------------
N.B. Aufgrund der Erfahrungen mit dem Herausgeber von "KI", Christaller,
auf  dessen  sachgemaesse  Bearbeitung  eines  damals  in  mod-ki  vorab
erschienenen Artikels ueber das Deduktionstreffen  1988  ich  bis  heute
vergeblich   warte,   ist  der  Abdruck  dieses  Beitrags  in  KI  nicht
automatisch gestattet: (c) 1989 Martin Weigele
************************************************************************