FORMAALIT MENETELMÄT 2003:

• Kurssille JA TENTTIIN ilmoittautuminen: Korpin kautta
• Surffauksen aloituspaikka: Formaalien menetelmien opetuksesta -sivu
• Aikamoinen kokoelma: Formaalien menetelmien -linkkejä (erityisesti työkaluja)
• Täältäkin pääsee pitkälle: NASA:n sivu formaaleista menetelmistä
• Vanha ohjelmistotuotannon www-sivukin on aika formaali: Ohjelmistotuotanto 2000
• Yksi aihepiiriä hipaiseva TKK:n kurssi, jonka yhteydestä löytyy myös hyvä linkkilista: Tik-76.611
• Löytyyhän näitä maailmaltakin...: CIS 771

Luentojen oheismateriaalia, lyhyt oppimäärä:

• Standard Template Library (STL) for C++:
  The Standard Template Library Tutorial by Johannes Weidl
  Mumit's STL Newbie guide
  
• Prototype Verification System (PVS): PVS homepage
• Larch: Larch Home Page
• HOL: The HOL theorem prover
• JML: The Java Modeling Language (JML) Home Page
• Daikon: The Daikon invariant detector
• ESC/Java: The Compaq Extended Static Checking for Java
• VDM: Information on The Vienna Development Method (VDM)
• Model Checking: e.g., at Carnegie Mellon, especially have a look at SMV

Luentokalvoja:

• Luento 1 (aloitusmessu): aloitus.pdf
• Luento 2 (käyttötapauksista): kalvo2.pdf
  • Basic Use Case Template, Basic Guidelines for Use Cases, Live debates on use cases
• Luento 3 (Yleistä FM:istä): kalvo3.pdf
  • Found from the web...
• Luento 4 (Sopimusohjelmoinnista jne.): kalvo4.pdf
• Luento 5 (Abstraktit tietotyypit): kalvo5.pdf
• Luento 6 (Formaalin systeemin kertausta): kalvo6.pdf (HUOM: Ei luentomonisteessa!)
  • Filosofiaa...
• Luento 7 (Propositiolaskennan kertausta): kalvo7.pdf (HUOM: Ei luentomonisteessa!)
• Luento 8 (Predikaattilaskennan kertausta): kalvo8.pdf (HUOM: Ei luentomonisteessa!)
  • Weppilogiikkaa...

• Tässä välissä monia luentoja, jotka perustuivat luentomoniste+taulu -tyyppiseen opetusmenetelmään...

• Luento n-1 (Estelle ja Lotos): kalvo14.pdf

• Luento n (SDL by Lari Kannisto): SDL_2003.pdf

• Luento n+1 (Cleanroom): kalvo15.pdf

Demoja:

Seminaari: