Beskjeder

Rom 8459 i 8. etg.   Oppmøtetider: 9:23 (SNS), 10:10 (ET), 11:10 (MB), 12:52 (ISL), 13:40 (FJO), 14:40 (FMDJ), 15:40 (LAW).  Lykke til!

Det ble ytret ønske om forelesning på fredag: hva har dere lært? var det noen sammenheng i emnet? 

I tillegg må vi snakke sette opp tidspunkter for eksamen 3/12. Alternativt kan alle møte 09:00 og vente hele dagen ...

Admin har nå lagt til en linje i undervisningsplanen :)

Jeg skal på IFI-julebord (første gangen på mange år) torsdag 27/11, men vi satser på en nyttig forelesning likevel. 

Som avtalt på forelesning er kildekoden til forelesning 7 tilgjengelig som http://olveczky.se/IN5100-25/Forelesninger/f25-7.tex .  Denne bruker de flotte figurene Drawing.png, prob-dist.png, oopsla22-header.png, a2pm-tool.png, a2pm-graphs.png, cointoss.jpg, simple-markov.jpg, mdp.jpg, papertiger.jpg, og tiger.jpg  som alle er tilgjengelig fra samme område.

Som bestemt på dagens forelesning er eksamen 3. desember. Funker også for sensor.

Nå har jeg endelig blitt ferdig med å definere pensum og, ikke minst, "spørsmål" man bør kunne besvare om disse delene av pensum.

Det tok litt tid, men tror dette ble et greit oppgavesett, og fint om man prøver å løse det før oppgavegjennomgang om en uke.

Obligatorisk oppgave 3 er ute, blir introdusert på forelesning 17/9, og har innleveringsfrist 24/10.

Beklager forsinkelsen, men her er obligatorisk oppgave 2, med innleveringsfrist 26. september. 

Husk: frist for obligatorisk oppgave 1 er 12. september!

Termer i objekt-orienterte systemer kan fort bli uleselige hvis de ikke blir vist på en "fin" måte.  Jeg har et litt grovt forslag til hvordan man får man fin output på OO termer.  Legg til følgende tre "format (...)" attributter til modulen CONFIGURATION nederst i filen "prelude.maude", som hos meg da blir:

mod CONFIGURATION is
  sorts Attribute AttributeSet .
  subsort Attribute < AttributeSet .
  op none : -> AttributeSet  [ctor] .
  op _,_ : AttributeSet AttributeSet -> AttributeSet
          [format (o m nssssssso o) ctor assoc comm id: none] .

  sorts Oid Cid Object Msg Portal Configuration .
  subsort Object Msg Portal < Configuration .
  op <_:_|_> : Oid Cid AttributeSet -> Object [ctor object
                                  ...

Vi fortsetter fredag 29/8 med oppgavene 7 og 8 i oppgavesett 1, og oppgave 1(a,b,d,e, h og i (de to siste temporallogikk, som vi kanskje skal snakke om på fredag)) i eksamen i IN2100, 2019.  Tenker at jeg også repeteter/introduserer litt temporallogikk.  

Neste uke er det forelesninger om meta-programmering.

Plan for den første delen av undervisningen er ute.  Her kan det bli endel endringer hvis jeg trenger å reise noe sted, og/eller basert på ønsker fra studentene.  Tenker vi starter med de tre obligatiske oppgavene (finne feil i kommunikasjonsprotokoll; meta-programmering; lage interpret til enkelt imperativt språk) i første delen av semesteret, og tar studentpresentasjoner av ymse temaer i emnets andre del.  Ligger an til undervisningsfri/jobbing med obliger i slutten av september.

Very tentative schedule for the first month published. There could be significant changes, based on my needs to travel for work, and/or wishes by the students. After intro to Maude, I guess we start with the three mandatory assignments (finding mistakes in published communication protocols; meta-programming; defining an intepreter/semantics for simple imperative languages) in the first part of the course, and student presentations of selected papers in the second...

Emnet ser på ulike aspekter ved formell modellering og analyse av distributerte systemer.  For eksempel ser vi på sanntidssystemer og probabilistiske systemer. Vi har også en introduksjon til meta-programmering. Som alltid: disse er fundamentale begreper som ikke er knyttet til omskrivningslogikk, men vi eksemplifiserer dem ved bruk av omskrivningslogikk (og formalismen og verktøyet Maude).  Vi studerer også hvordan man kan definere semantikken/en interpret til et programmeringsspråk i Maude.  Til sist ser vi på endel eksempler på bruk av formelle metoder til ymse systemer, som for eksempel cloud-baserte transaksjonssystemer, modellering av biokjemiske reaksjoner, analyse av smarte kontrakter, hvordan knekke web browsere og VISA/MasterCard ved bruk av formelle metoder, finne feil i DNS, og så videre.  Vi starter med repetisjon/kort introduksjon av Maude, og deretter ser om vi kan knekke en liten publisert kommunikasjonsprotokoll.  Deretter noen felles...