1. Ambrus Kaposi
  2. agdaoktatas

Overview

HTTPS SSH

Miről szól ez a tantárgy?

Program helyes működésének biztosítása:

  • a program futtatása különböző bemenetekkel és a kimenetek ellenőrzése

    Java JUnit framework

  • a program futás idejű monitorozása

    Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException
    
  • a program egy egyszerűsített modelljének szimulálása, és annak ellenőrzése, hogy a szimulált világ lehetséges állapotaiban megfelelő programműködést tapasztalunk -e

    NuSMV

    state : {ready, busy}, request : boolean
    init(state) := ready
    next(state) := if state = ready & request = TRUE
    then busy else {ready, busy}
    
  • a program részleges specifikálása típusokkal, és a program fordítása során ennek a specifikációnak való megfelelés ellenőrzése

    4 : Int
    
    [1,2,4] : List Int
    
    (+) 4 : Int  Int
    
    length : String  Int
    
  • a program helyességének bizonyítása formális eszközökkel vagy bizonyítottan helyes program szintézise

    B módszer, Isabelle, Coq

Mi a típusrendszer használatával foglalkozunk.

Típusok:

length : String → Int         "hello" : String
----------------------------------------------
              length hello : Int

plus : Int × Int → Int        (2 , 3) : Int × Int
-------------------------------------------------
              plus (2 , 3) : Int

List : Type → Type

lengthInt    : List Int    → Int
lengthChar   : List Char   → Int
lengthString : List String → Int

length : (A : Type) → List A → Int

Haskellben megadható a négyzetes mátrixok típusa (de bonyolult)

Az alábbi típusok már nem:

  • fix-hosszú listák (tömbből ne lehessen kiindexelni)

  • rendezett listák

  • kiegyensúlyozott fák, AVL-fák, B-fák

  • 13 és 45 közötti számok

Agdában ezek is megadhatók.

Példa ugyanarra a programra, egyre kifinomultabb típusokkal:

sort : List Int  List Int

sort : List Int  SortedList Int

sort : (xs : List Int)  (ys : SortedList Int) × (length xs = length ys)

sort : (xs : List Int)  (ys : SortedList Int) × (length xs = length ys) × (x  xs  x  ys)

sort : (xs : List Int)  (ys : SortedList Int) × (length xs = length ys) × (x  xs  x  ys)

sort : (xs : List Int)  (ys : SortedList Int) × (ys `permutationOf` xs)

Tematika:

  • nulladrendű logika

  • elsőrendű logika

  • klasszikus logika

  • funkcionális programozás Agdában

  • induktív típusok

  • koinduktív típusok

Cél:

  • bizonyítottan helyes gyorsrendezés

Számonkérés:

  • beadandó kiírása minden héten óra után, két héttel később beadási határidő

  • vizsgán Agda programozás

Egyéb:

  • kísérleti fázis

  • kérdezzetek

Gyakorlati dolgok

Telepítés:

Emacs használat:

Feladatok: