.md .pdf

Vsebina

10. Specifikacija, implementacija, abstrakcija

10.1. Specifikacija & implementacija

Specifikacija (angl. specification) S je zaheva, ki opisuje, kakšen izdelek želimo.

Implementacija (angl. implementation) I je izdelek. Implementacija I zadošča specifikaciji S, če ustreza zahtevam iz S.

V programiranju je implementacija programska koda. Specifikacije podajamo na različne načine in jih pogosto razvijemo postopoma:

• pogovor s stranko in analiza potreb

• dokumentacija, ki jo razume stranka

• tehnična dokumentacija za programerje

Brez specifikacije ne vemo, kaj je treba naprogramirati. Danes si bomo ogledali, kako v programskih jezikih poskrbimo za zapis specifikacij in kako programski jezik preveri, ali dana koda (implementacija) zadošča dani specifikaciji.

Omenimo še povezavo z algebro. V algebri poznamo algebraične strukture, na primer vektorske prostore, grupe, monoide, kolobarje, Boolove algebre, … Definicija takih struktur poteka v dveh korakih:

• signatura pove, kakšne množice, konstante in operacije imamo

• aksiomi povedo, kakšnim zakonam morajo zadoščati operacije

Primer

Matematično strukturo grupa opišemo takole:

• signatura:

  • množica G

  • operacija · : G × G → G

  • operacija ⁻¹ : G → G

  • konstanta e : G

• aksiomi:

    x · (y · z) = (x · y) · z
    x · e = x
    e · x = x
    x · x⁻¹ = e
    x⁻¹ · x = e
  

Primer

Matematično strukturo usmerjen graf opišemo takole:

• signatura:

  • množica V (vozlišča)

  • množica E (povezave)

  • operacija src : E → V (začetno vozlišče povezave)

  • operacija trg : E → V (končno vozlišče povezave)

• aksiomi: ni aksiomov

Zakaj vse to razlagamo? Ker programski jeziki ponavadi omogočajo zapis signature v programskem jeziku, ne pa tudi aksiomov, saj jih prevajalnik ne more preveriti.

10.2. Vmesniki

Specifikaciji včasih rečemo tudi vmesnik (angl. interface), ker jo lahko razumemo kot opis, ki pove, kako se uporablja neko programsko kodo. Na primer, avtor programske knjižnice običajno objavi API (Application Programming Interface), ki ni nič drugega kot specifikacija, ki pove, kako deluje knjižnica.

Torej imamo (vsaj) dve uporabi specifikacij:

• zahtevek za programsko kodo (specifikacija)

• protokol za uporabo programske kode (vmesnik)

10.2.1. Vmesniki v Javi

V Javi je specifikacija S podana z vmesnikom

public interface S {
   ...
}

v katerem lahko naštejemo metode. Tipe, ki nastopajo v specifikaciji, podamo kot generične razrede. Na primer, vmesnik za grupo bi zapisali takole:

public interface Group<G> {
    public G getUnit();
    public G multiply(G x, G y);
    public G inverse(G x);
}

Vmesnik za usmerjeni graf:

public interface Graph<V, E> {
    public V src(E e);
    public V trg(E e);
}

Seveda v praksi nihče ne piše takih vmesnikov, tu samo razmišljamo o zvezi med matematičnimi signaturami in vmesniki v programskih jezikih. Kasneje bomo videli bolj uporabne vmesnike, ki opisujejo abstraktne podatkovne strukture.

10.2.2. Vmesniki v OCamlu

V OCamlu lahko podamo poljubno signaturo (tipe in vrednost), ne moremo pa zapisati aksiomov, ki jim zadoščajo. Takole zapišemo signaturo za grupo:

module type GROUP =
sig
  type g
  val mul : g * g -> g
  val inv : g -> g
  val e : g
end

In takole za usmerjeni graf:

module type DIRECTED_GRAPH =
sig
  type v
  type e
  val src : e -> v
  val trg : e -> v
end

10.3. Implementacija

Programski jeziki seveda omogočajo implementacijo, kar ni nič drugega kot pisanje kode, ki ustreza dani specifikaciji. Zanimivo pa je vprašanje, kako so posamezne enote implementacije organizirane v različnih jezikih.

10.3.1. Implementacija v Javi

V Javi implementiramo vmesnik I tako, da definiramo razred C, ki mu zadošča:

public class C implements I {
   ...
}

Razred lahko hkrati zadošča večim vmesnikom. (Opomba: podrazredi so mehanizem, ki se ne uporablja za specifikacijo.)

10.3.2. Implementacija v OCamlu

Implementacija v OCamlu se imenuje modul (angl. module). Modul je skupek definicij tipov in vrednosti, lahko pa vsebuje tudi še nadaljnje podmodule.

Nekaj primerov (nepraktičnih) implementacij grup podajmo tu, kasneje pa bomo videli bolj uporabne primere:

(* Najprej definiramo signature. *)

module type GROUP =
sig
    type g
    val mul : g * g -> g
    val inv : g -> g
    val e : g
end

module type DIRECTED_GRAPH =
sig
    type v
    type e
    val src : e -> v
    val trg : e -> v
end

(* Signaturo implementiramo z modulom ali strukturo.
   Dana signatura ima lahko več implementacij. *)

module Z3 : GROUP =
struct

  type g = Zero | One | Two

  let e = Zero

  let plus = function
    | (Zero, y) -> y
    | (x, Zero) -> x
    | (One, One) -> Two
    | (One, Two) -> Zero
    | (Two, One) -> Zero
    | (Two, Two) -> One

  let mul = plus

  let inv = function
    | Zero -> Zero
    | One -> Two
    | Two -> One
end

module Z3' : GROUP =
struct

    type g = int

    let mul (x, y) = (x + y) mod 3
    let inv x = (3 - x) mod 3
    let e = 0
end

module K4 : DIRECTED_GRAPH =
struct

    type v = V0 | V1 | V2 | V3
    type e = E0 | E1 | E2 | E3 | E4 | E5

    let src = function
      | E0 -> V0
      | E1 -> V1
      | E2 -> V2
      | E3 -> V3
      | E4 -> V0
      | E5 -> V1

    let trg = function
      | E0 -> V1
      | E1 -> V2
      | E2 -> V3
      | E3 -> V0
      | E4 -> V2
      | E5 -> V3
end

module Cycle3 : DIRECTED_GRAPH =
struct
  type v = int (* uporabimo 0, 1, 2 *)
  type e = int (* uporabimo 0, 1, 2 *)
  let src e = e
  let trg e = (e + 1) mod 3

  (* Graf z vozlišči 0, 1, 2 in povezavami 0, 1, 2:
        src    trg
     0 : 0 --> 1
     1 : 1 --> 2
     2 : 2 --> 0
  *)
end

(* Takole pa naredimo modul, ki je parametriziran s
   strukturo. Kasneje bomo videli bolj uporabne primere. *)
module Cycle (S : sig val n : int end) : DIRECTED_GRAPH =
struct
  type v = int
  type e = int
  let src k = k
  let trg k = (k + 1) mod S.n
end

module C5 = Cycle(struct let n = 5 end)
module C15 = Cycle(struct let n = 15 end)

10.4. Abstrakcija

Ko gradimo večje programske sisteme, so ti sestavljeni iz enot, ki jih povezujemo med seboj. Za vsako enoto je lahko zadolžena ločena ekipa programerjev. Programerji opišejo programske enote z vmesniki, da vedo, kaj kdo počne in kako uporabljati kodo ostalih ekip.

A to je le del zgodbe. Denimo, da prva ekipa razvija programsko enoto E, ki zadošča vmesniku S in da druga ekipa uporablja enoto E pri izdelavi svoje programske enote. Dobra programska praksa pravi, da se druga ekipa ne sme zanašati na podrobnosti implementacije E, ampak samo na to, kar je zapisano v specifikaciji S. Na primer, če E vsebuje pomožno funkcijo f, ki je S ne omenja, potem je druga ekipa ne sme uporabljati, saj je f namenjena notranji uporabi E. Prva ekipa lahko f spremeni ali zbriše, saj f ni del specifikacije S.

Če sledimo načelu, da mora programski jezik neposredno podpirati aktivnosti programerjev, potem bi želeli skriti podrobnosti implementacije E tako, da bi lahko programerji druge ekipe imeli dostop samo do tistih delov E, ki so našteti v S.

Kadar skrijemo podrobnosti implementacije, pravimo, da je implementacija abstraktna.

Programski jeziki omogočajo abstrakcijo v večji ali manjši meri:

• Java nadzoruje dostopnost do komponent z določili private, public in protected

• Python nima nikakršne abstrakcije

• OCaml omogoča abstrakcijo z določilom M : S, kjer je M module in S signatura. S tem skrijemo vsebino modula M, razen tistih komponent, ki so naštete v S.

10.5. Generično programiranje

Z izrazom generično programiranje razumemo kodo, ki jo lahko uporabimo večkrat na različne načine. Na primer, če napišemo knjižnico za 3D grafiko, bi jo želeli uporabljati na več različnih grafičnih karticah. Ali bomo za vsako grafično kartico napisali novo različico knjižnice? Ne! Želimo generično implementacijo, ki bo preko ustreznega vmesnika dostopala do grafične kartice. Proizvajalci grafičnih kartic bodo implementirali gonilnike, ki bodo zadoščali temu vmesniku.

10.5.1. Generično progarmiranje v Javi

Java podpira generično programiranje. Ko definiramo razred, je ta lahko odvisen od kakega drugega razreda:

public class Knjiznica3D<Driver extends GraphicsDriver> {
  ...
}

10.5.2. Generično programiranje v OCamlu

V OCamlu je generično programiranje omogočeno s funktorji (angl. functor) (opomba: v matematiki poznamo funktorje v teoriji kategorij, ki nimajo nič skupnega s funktorji v OCamlu).

Funktor je preslikava iz struktur v strukture in je bolj splošen kot generični razredi v Javi (ker lahko struktura vsebuje podstrukture in definicije večih tipov, razred pa ne more vsebovati definicij podrazredov).

Funktor F, ki sprejme strukturo A, ki zadošča signaturi S, in vrne strukturo B zapišemo takole:

module F(A : S) =
struct
  ⟨definicija strukture B⟩
end

Zgoraj smo videli primer preprostega funktorja Cycle, ki sprejme strukturo s številom n in vrne usmerjeni cikel na n vozliščih. Bolj uporaben primer sledi.

10.6. Primer: prioritetne vrste

Prioritetna vrsta je podatkovna struktura, v katero dodajamo elemente, ven pa jih jemljemo glede na njihovo prioriteto. Zapišimo specifikacijo:

Signatura:

• podatkovni tip element

• operacija priority : element → int

• podatkovni tip queue

• konstanta empty : queue

• operacija put : element → queue → queue

• operacija get : queue → element option * queue

Aksiomov ne bomo pisali, ker bi morali v tem primeru spoznati bolj zahtevne jezike za specifikacijo, ki presegajo okvir te lekcije. Neformalno pa lahko opišemo zahteve za prioritetno vrsto:

• element je tip elementov, ki jih hranimo v vrsti

• priority x vrne prioriteto elementa x, ki je celo število. Manjše število pomeni »prej na vrsti«

• queue je tip prioritetnih vrst

• empty je prazna prioritetna vrsta, ki ne vsebuje elementov

• put x q vstavi element x v vrsto q glede na njegovo prioriteto in vrne tako dobljeno vrsto

• get q vrne (Some x, q') kjer je x element iz q z najnižjo prioriteto in q' vrsta q brez x Operacija get vrne (None, q), če je q prazna vrsta.

10.6.1. Implementacija v OCamlu

Oglejmo si implementacijo v OCamlu.

module type PRIORITY_QUEUE =
  sig
    type element
    val priority : element -> int
    type queue
    val empty : queue
    val put : element -> queue -> queue
    val get : queue -> element option * queue
  end

module MyFirstQueue : PRIORITY_QUEUE with type element = int * int =
  struct
    type element = int * int

    let priority (a, b) = a

    type queue = element list

    let empty = []

    let rec put x = function
      | [] -> [x]
      | y :: ys ->
         if priority x <= priority y then
           x :: y :: ys
         else
           y :: put x ys

    let get = function
      | [] -> (None, [])
      | x :: xs -> (Some x, xs)
  end

module type PRIORITY =
sig
  type t
  val priority : t -> int
end


(* Implementacija prioritetne vrste s seznami. To je funktor, ki
   sprejme tip elemetov in prioritetno funkcijo. *)
module ListQueue (M : PRIORITY) : PRIORITY_QUEUE with type element = M.t
  =
  struct
    type element = M.t

    let priority = M.priority

    type queue = element list

    let fortytwo = 42

    let empty = []

    let rec put x = function
      | [] -> [x]
      | y :: ys ->
         if priority x <= priority y then
           x :: y :: ys
         else
           y :: put x ys

    let get = function
      | [] -> (None, [])
      | x :: xs -> (Some x, xs)
  end

(* Naredimo prioritetno vrsto nizov, prioriteta je dolžina niza. *)
module A =
  ListQueue(
      struct
        type t = string
        let priority = String.length
      end)

(* Preizkus. *)
let example1 =
  A.get (A.put "kiwi" (A.put "jabolko" (A.put "banana" A.empty)))

(* Naredimo prioritetno vrsto nizov, prioriteta je dolžina niza. *)
module A' =
  ListQueue(
      struct
        type t = string
        let priority s = - String.length s
      end)

(* Preizkus. *)
let example1' =
  A'.get (A'.put "kiwi" (A'.put "jabolko" (A'.put "banana" A'.empty)))

(* Naredimo prioritetno vrsto parov števil. *)
module B =
  ListQueue(
      struct
        type t = int * int
        let priority (a,b) = a
      end
    )

module IntQueue =
  ListQueue(
    struct
      type t = int
      let priority k = k
    end
  )


(* Učinkovita implementacija z levičarskimi kopicami,
   glej https://en.wikipedia.org/wiki/Leftist_tree.
   Implementacija je abstraktna, ker uporabimo :,
   vendar dodamo določilo, da je tip element enak tipu t.
 *)
module LeftistHeapQueue (M : PRIORITY)
       : PRIORITY_QUEUE with type element = M.t =
  struct
    type element = M.t

    let priority = M.priority

    type queue = Leaf | Node of int * element * queue * queue

    let rank = function
      | Leaf -> 0
      | Node (r, _, _, _) -> r

    let node (x, a, b) =
      if rank a < rank b then
        Node (1 + rank a, x, b, a)
      else
        Node (1 + rank b, x, a, b)

    let rec meld a b =
      match (a, b) with
      | (_, Leaf) -> a
      | (Leaf, _) -> b
      | (Node (_, ka, la, ra), Node (_, kb, lb, rb)) ->
         if priority ka < priority kb then
           node (ka, la, meld ra b)
         else
           node (kb, lb, meld a rb)

    let singleton x = Node (1, x, Leaf, Leaf)

    let empty = Leaf

    let put x q = meld q (singleton x)

    let get = function
      | Leaf -> (None, Leaf)
      | Node (_, y, l, r) -> (Some y, meld l r)
  end


module D = LeftistHeapQueue(
               struct
                 type t = int * int
                 let priority (x, y) = x + y
               end)

let example2 =
  let rec loop q = function
    | 0 -> D.put (0, 0) q
    | k -> loop (D.put ((47 * k * k + 13) mod 1000, k) q) (k - 1)
  in
  loop D.empty 300000

let rec to_list q =
  match D.get q with
  | (None, _) -> []
  | (Some x, q) -> x :: to_list q

10.6.2. Implementacija v Javi

Oglejmo si še implementacijo v Javi. V tem jeziku je bolj naravno narediti vrste kot objekte, ki se spreminjajo. Torej spremenimo specifikacijo.

Signatura:

• podatkovni tip Element

• metoda priority : element → int

• podatkovni tip queue

• operacija empty : unit → queue

• operacija is_empty : queue → bool

• operacija put : element → queue → unit

• operacija get : queue → element option

Zahteve so podobne kot prej, le da operacije empty, put in get delujejo nekoliko drugače:

• empty () vrne nov primerek (objekt) prazne vrste

• put x q vstavi x v vrsti q in s tem spremeni q

• get q vrne prvi x v vrsti q in s tem spremeni q

Zgornjo specifikacijo predelamo v dva vmesnika. Prvi je vmesnik za razrede, ki imajo metodo priority:

public interface Priority {
	public int priority();
}

Vmesnik PriorityQueue pa podaja specifikacijo za prioritetno vrsto:

public interface PriorityQueue<Element extends Priority> {
    public PriorityQueue<Element> emptyQueue();
    public boolean isEmpty();
    public void put(Element x);
    public Element get();
}

Še primer implementacije prioritetnih vrst s seznami:

import java.util.LinkedList;

public class ListQueue<Element extends Priority> implements PriorityQueue<Element> {
    private LinkedList<Element> elements;

    public ListQueue() {
        elements = new LinkedList<Element>();
    }

    @Override
    public boolean isEmpty() {
        return elements.isEmpty();
    }

    @Override
    public void put(Element x) {
        int i = 0;
        for (Element y : elements) {
            if (x.priority() < y.priority()) {
                break;
            } else {
                i += 1;
            }
        }
        elements.add(i, x);
    }

    @Override
    public Element get() {
        return elements.removeFirst();
    }

    @Override
    public PriorityQueue<Element> emptyQueue() {
        return new ListQueue<Element>();
    }
}

10.7. Primer: množice

Na vajah boste na dva načina implementirali končne množice, opisane z naslednjo signaturo: signaturo.

type order = Less | Equal | Greater

module type SET =
sig
    type element
    val cmp : element -> element -> order
    type set
    val empty : set
    val member : element -> set -> bool
    val add : element -> set -> set
    val remove : element -> set -> set
end

nazaj

9. Logično programiranje z omejitvami

naprej

11. Podtipi in objekti