I222 - Semantikk til programmeringsspråk

Oppgavesett 5, vår 2000

  1. Typesjekking av program er i læreboken skissert som en del av kjøretidssemantikken til programmet, seksjon 9.5. Typesjekking kan alternativt legges inn som et eget lag i semantikken (og med separat typesjekk kan vi bruke den utypede semantikken for kjøretidssemantikken, se seksjon 9.1). Det kan gjøres ved å skrive en semantikk til produksjonene som bare fanger typeinformasjon. Semantikkfunksjonene vil da ikke gi informasjon om resultatet av å utføre et program, men om typene i programmet. En måte å gjøre dette på er, med utgangspunkt i Decl0 (figur 9.1 s. 189), å ha typesemantiske funksjoner 
    	TP: Prog -> TypeOK
	TM: Imp -> Tenvir -> TypeOK
	TD: Decl -> Tenvir -> Tenvir
	TT: Vartype -> Type
	TE: Exp -> Tenvir -> Type
	TV: Var -> Ident
	TBO: Binop -> (Type × Type × Type) 
	TUO: Unop -> (Type × Type)
	TA: Literal -> Type
    Etter mønster fra boken kan vi definere typeomgivelsen og de typesemantiske domenene som følger: 
    	TypeOK = true: Unit + false: Unit
	Type = typeint: Unit + typebool: Unit + typeerror: Unit
	T = tvar: Type + tconst: Type + undeclared: unit
	Tenvir = Ident -> T
    Domenet Tenvir har de vanlige funksjonene Void: -> Tenvir for å lage en typeomgivelse som gir undeclared for alle identifikatorerer, og bind: (Tenvir × Ident × Type) -> Tenvir for å legge en ny identifikator til typeomgivelsen (slik som i figur 9.3 s. 193 for vanlige omgivelser). De typesemantiske funksjonene defineres for hver produksjon, som vanlig for semantiske funksjoner: 
    	TP[[ imp ]] = TM [[imp]] Void

	TM[[ skip        ]] tenv = true
	TM[[ put exp     ]] tenv = { true       for typeint=TE[[exp]] tenv, 
	                           { false      otherwise
	TM[[ get var     ]] tenv = { true       for tvar(typeint)=tenv(TV[[var]]), 
	                           { false      otherwise
	TM[[ var := exp  ]] tenv = { true       for tvar(tl)=tenv(TV[[var]]), 
	                           {                tr=TE[[exp]] tenv,
	                           {                tl=tr
	                           { false      otherwise
	TM[[ imp1 ; imp2 ]] tenv = { true       for true=TM[[imp1]] tenv, 
	                           {                true=TM[[imp2]] tenv
	                           { false      otherwise
	TM[[ begin decl; imp end ]] tenv = TM[[imp]] (TD[[decl]] tenv)
	TM[[ if exp
	     then imp1
	     else imp2   ]] tenv = { true       for tr=TE[[exp]] tenv, 
	                           {                typebool=tr,
	                           {                true=TM[[imp1]] tenv,
	                           {                true=TM[[imp2]] tenv
	                           { false      otherwise
	TM[[ while exp
	     do imp      ]] tenv = { true       for tr=TE[[exp]] tenv, 
	                           {                typebool=tr,
	                           {                true=TM[[imp]] tenv
	                           { false      otherwise

	TD[[ const id = lit ]] tenv = bind(tenv,id,tconst typeint)
	TD[[ var id : vtype ]] tenv = bind(tenv,id,tvar   TT[[vtype]])
	TD[[ decl1 ; decl2  ]] tenv = TD[[decl2]] (TD[[decl1]] tenv)

	TT[[ int  ]] = typeint
	TT[[ bool ]] = typebool

	TE[[ lit         ]] tenv = TA[[lit]]
	TE[[ id          ]] tenv = { tl         for tvar  (tl)=tenv(id)
	                           { tr         for tconst(tr)=tenv(id)
	                           { typeerror  otherwise     
	TE[[ ex1 bop ex2 ]] tenv = { tres       for (targ1,tright,targ2)=TBO[[bop]],
	                           {                tex1=TE[[ex1]] tenv,
	                           {                tex1=targ1,
	                           {                tex2=TE[[ex2]] tenv,
	                           {                tex2=targ2,
	                           { typeerror  otherwise
	TE[[ uop ex      ]] tenv = { tres       for (targ,tres)=TUO[[uop]],
	                           {                tex=TE[[ex]] tenv,
	                           {                tex=targ
	                           { typeerror  otherwise

	TV[[ id ]] = id

	TBO[[ + ]] = (typeint, typeint, typeint)
	TBO[[ - ]] = (typeint, typeint, typeint)
	TBO[[ * ]] = (typeint, typeint, typeint)
	TBO[[ / ]] = (typeint, typeint, typeint)
	TBO[[ = ]] = (typeint, typeint, typebool)
	TBO[[ < ]] = (typeint, typeint, typebool)

	TUO[[ - ]] = (typeint, typeint)
	TUO[[ ¬ ]] = (typebool, typebool)

	TA[[ lit ]] = typeint
    Skriv dette som et ML-program for å teste typekorrekthet til program skrevet i Decl0.

  2. Definer typesemantikk (slik som i forrige oppgave) for språket Loop, figur 2.1 s. 8.
    Skriv dette som et ML-program.

  3. Definer typesemantikk (slik som i forrige oppgave) for språket While, figur 6.1 s. 101.
    Skriv dette som et ML-program.

  4. Definer typesemantikk (slik som i forrige oppgave) for språket Decl1, seksjon 9.1 s. 217. Husk at vi ikke kan sjekke om en indeks er innenfor eller utenfor en tabell før ved kjøretid.
    Skriv dette som et ML-program.

  5. Definer typesemantikk (slik som i forrige oppgave) for språket Proc0, figur 10.1 s. 232. Her kan du la parametermodus inngå i typeinformasjonen til en prosedyre.
    Skriv dette som et ML-program.

  6. Definer et språk som integrerer språkbegrepene fra Decl1 og Proc0, dvs. et språk med både array og prosedyrer/funksjoner. Tillat prosedyrene/funksjonene å 0, 1, 2 eller flere parametre.
    Definer en typesemantikk for dette språket.
    Definer en kjøretidssemantikk for dette språket.
    Skriv dette som et ML-program.

  7. Se Allison seksjon 4.3.2. Vi skal her bevise de egenskapene boken skisserer og som vi begynte å se på på forelesningen 15.5.00. Egenskapene kan vises ved induksjon over , med start med i=0.

Sist oppdatert 2000-05-25 av Magne Haveraaen