[an error occurred while processing this directive]

IN217: Programspesifikasjon og -verifikasjon
Vår 2001


Forelesere: Peter Ölveczky (epost: peterol@ifi.uio.no)
  Olaf Owe (epost: olaf@ifi.uio.no)
Gruppelærer: Thomas Wold Hansen (epost: thomaha@ifi.uio.no)
Viktig informasjon: Læremidler og pensum
  Emnebeskrivelse
  Tidligere eksmanesoppgaver: in215, in217 samt eksamen 2001 med løsningsforslag .
  Tid og sted
Obligatoriske oppgaver: Oblig1-first 4.4. (Se under)  Godkjentliste
Eksamen: 8. juni 2001

Plan for kurset:

Alle forelesningsnotatene finnes både i pdf-format (som anbefales for skjermbruk) og i dvi-format (som anbefales for utskrift, med f eks print -l -multi4 ). Ukeoppgavene gjennomgås uken etter forelesningene. Dermed tilhører oppgavene for uke 5 til forelesningene for uke 4, osv.
Merk at vi i år har valgt et "top-down" kursopplegg, der kap 4 (Hoare-logikk) taes til slutt.
Uke Tema Foiler Ev. ekstra notater Oppgaver som gjennomgås på gruppene
22-24.1 Introduksjon, motivasjon og eksempler pdf, dvi    
29-31.1 Formallogikk:
Formelle bevis og sekventkalkyle 		pdf, dvi
pdf, dvi 		dvi
dvi 		Oppgavesett 1 (løsningsforslag)
5-7.2 Formelle bevis og sekventkalkyle.
Datatyper: typer, subtyper, definerthet, TGI 		 
pdf, dvi 		 
dvi 		Oppgavesett 2 (løsningsforslag)
12-14.2 Datatyper: typer, subtyper, definerthet, TGI     Oppgavesett 3 (løsningsforslag)
19-21.2 Datatyper: termomskrivning, induksjon
(Ingen forelesning 21.2)		 pdf, dvi   Oppgavesett 4 (løsningsforslag)
26-28.2 Datatyper: likhet (ad hoc, TGI, obsbas, kanonisk), definerthet pdf, dvi   Oppgavesett 5 (Eksamen 1996) (løsningsforslag)
5-7.3 Datatyper: typemoduler og generatorinduksjon pdf, dvi   Endelig oppgavesett 6 (Eksamen 1993) (løsningsforslag)(løsningsforslag eks93, oppgave 1)
12-14.3 Datatyper: typesimulering pdf, dvi   Oppgavesett 7 (løsningsforslag)
19-21.3 Datatyper: typesimulering pdf, dvi   Oppgavesett 8 (Eksamen 1993) (Eksamen 1994) (se eksamensoppgavesiden for løsningsforslag til eksamensoppgaver)
26-28.3 Objekter og klasser pdf, dvi   Oppgavesett 9 (løsningsforslag)
2-4.4 Arrays. Hoare logikk (husk oblig1-frist 4.4!) pdf, dvi   Oppgavesett 10 (løsningsforslag)
9-11.4 Påske-ferie
18.4 Hoare-logikk: introduksjon     Ingen øvelser
23-25.4 Hoare-logikk: if-, og while-setninger pdf, dvi   Oppgavesett 11 (det første om Hoare-logikk)(løsningsforslag)
30.4-2.5 Hoare-logikk: lokale variable, for-setning, hopp pdf, dvi   Oppgavesett 12 (det andre om Hoare-logikk) (løsningsforslag)
7-9.5 Hoare-logikk: adaptering, effektfunksjoner, prosedyrer pdf, dvi   Oppgavesett 13 (det tredje om Hoare-logikk)(løsningsforslag)
14-16.5 Hoare-logikk: mytiske avsnitt, ikke-determinisme og input/output pdf, dvi pdf, dvi   Oppgavesett 14 (det fjerde om Hoare-logikk)(løsningsforslag)
23.5 Spørsmål fra salen     Oppgavesett 15 (det femte om Hoare-logikk)(løsningsforslag)
28-29.5       Eksamen 1998 (Se eksamensoppgavesiden)
8.6 Eksamen

Grupper

Kun gruppe 1 (mandag 9.15-11, tirsdag 15.15-17, begge ganger i lille auditorium) er åpen.

Obligatoriske oppgaver

Endelig er det klart for obligatorisk oppgave 1. På forespørsel ble dette oppgave 1-a til og med oppgave 1-i i Eksamen 2000. Oppgaven skal leveres senest onsdag 4.4.2001 kl. 1800 til gruppelærer. Foreleser har ingenting med obligatorisk oppgave å gjøre. Man kan løse oppgaven en og en, eller i grupper om to. Slike grupper leverer bare en besvarelse. Kopiering eller andre forsøk på juks vil føre til minst utelukkelse fra kurset.

Meldinger

Siste meldinger legges øverst.

Andre morsomme ting som ikke er pensum

Generelt



Sist oppdatert Monday, 18-Jun-2001 12:02:03 CEST av Peter Ölveczky / Olaf Owe