Bergen, 7. Juli 1996

• Contents
• KATEGORITEORI
  • Noen enkle eksempler
  • Initielle objekter og terminalobjekter
  • Produkt
  • Sum
  • Funktorer
    • Eksempler på funktorer
  • Naturlige transformasjoner
  • Adjungerte funktorer
• ALGEBRAISK SPESIFIKASJON
  • Spesifikasjon
    • Et eksempel
    • Sammensetning av spesifikasjoner
  • Algebra
    • Omvendt sammenheng
    • Term, kvotient og initielle algebraer
• Litt om Larch
  • LSL
    • Kortformen tuple
    • Alle funksjoner er totale i LSL
    • Larchs bibliotek av traiter
  • LP
    • Definering av teorien
    • Utførelsen av bevis
  • LCPP
    • Spesifikasjon av funksjoner
  • Sammenhengen mellom LSL, LP og LCPP
• Introduksjon til ATLASII
  • Syntax til ATLASII spesifikasjoner
    • Mer avanserte muligheter
      • Modulens type system
      • Parametre
      • Exportdelen
      • Importdelen
      • Hoveddelen til en modul
  • Subtyping
  • Bruk av ATLASII
• Noen begreper i algebraisk spesifikasjon
  • Sort og type
  • 1. ordens logikk
  • Sproget til en spesifikasjon
  • Teorien til en trait
  • Hva spesifikasjonen ikke sier
  • Konsistens og kompletthet
    • Komplett-definert
  • Omskrivning
• Strategier ved spesifikasjon
  • Spesifikasjonsstrategier
  • Partielle operatorer
  • Subtyping
    • Order-sorted algebra
    • Syntaktisk subtyping
    • Subtyping i LSL
  • Voktede algebraer
    • Noe matematiske teori ved voktede algebraer
    • Voktede algebraer i praksis
  • Andre måter
  • Standard strategi i LSL
    • Betingede og ubetingede aksiomer
  • Strategi i ATLAS
  • Hvordan spesifikasjonene er utformet
    • Generatorene
    • observatorene
    • aksiomene
    • Høyresidene i ligningene
    • Hva vet en så om spesifikasjonene
• ATLASII vs. LSL
  • Syntaktiske forskjeller
    • Formen på aksiomene
  • Høyere orden
  • Allerede tilgjengelige spesifikasjoner
  • Initielle modeller
• Spesifikasjoner av klasser i Sophus
  • Klassen MeshShape
    • Bevis av implies-delen
    • LCPP-spesifikasjonen av MeshShape
  • Klassen MeshPoint
    • Bevis for sameShape(point,MeshPoint(shape)) => MeshPoint(shape) + point = point:
  • Klassen elem og elemField
  • Klassen meshCont
  • Klassen meshScalarField
  • Klassen array
• Bevis av implementasjoner
  • Bevis av meshCont
    • Den implementasjonsrettede spesifiseringen av meshCont
    • Sammenheng mellom punkter og heltall
    • Mer om MCA
    • Beviset
  • Bevis av meshScalarField
  • Konklusjon
• Fremgangsmåte ved utvikling av numerisk programvare
  • Begynnelsen
  • LSL-spesifikasjonen
  • LCPP-spesifikasjonen
  • Uformelt design
  • Formelt design
• Oppsummering og konklusjon
• About this document ...