Objektorientierte und funktionale Softwareentwicklung ... Refactoring von Java Legacy Code Clean...

download Objektorientierte und funktionale Softwareentwicklung ... Refactoring von Java Legacy Code Clean Code

If you can't read please download the document

  • date post

    28-Jun-2020
  • Category

    Documents

  • view

    1
  • download

    0

Embed Size (px)

Transcript of Objektorientierte und funktionale Softwareentwicklung ... Refactoring von Java Legacy Code Clean...

  • Objektorientierte und funktionale Softwareentwicklung Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und

    Domain-Driven Design Facilitation von Code Retreats und

    Legacy Code Retreats

  • Michael Sperber

    • funktionale Programmierung

    • Scala, Clojure, F#, Haskell, OCaml, Erlang, Elixir, Swift

    • Schulungen und Coaching

    • Blog: funktionale-programmierung.de

    • Entwickerkonferenz BOB bobkonf.de

  • "IoT Goes Nuclear: Creating a ZigBee Chain Reaction"

    http://iotworm.eyalro.net/

  • https://www.arbornetworks.com/blog/asert/mirai-iot-botnet-description-ddos-attack-mitigation/

  • http://heartbleed.com/

  • https://www.wired.com/2015/07/hackers-remotely-kill-jeep-highway/

  • http://wp.doc.ic.ac.uk/riapav/wp-content/uploads/sites/28/2014/05/HACMS-Fisher.pdf

  • User Stories "We will do what is needed and asked for, but no more."

    FIXME

    http://www.extremeprogramming.org/values.html

  • Korrekte Software – wie?

  • Intel Pentium, FDIV-Bug

  • Listen data List: (a:Type) -> Type where

    Nil : List a

    (::) : a -> List a -> List a

  • Listen mapL : (a -> b) -> List a -> List b

    mapL f [] = []

    mapL f (x :: xs) = f x :: mapL f xs

  • Nicht-Termination x : a

    x = x

  • Vektoren data Vect : (n:Nat) -> (a:Type) -> Type where

    Nil: Vect 0 a

    (::) : a -> Vect n a -> Vect (n+1) a

  • Automatische Herleitung Implementierung mapV : (a-> b) -> Vect n a -> Vect n b

    mapV f [] = []

    mapV f (x :: xs) = f x :: mapV f xs

  • Element-Test herleiten? isElemF : a -> Vect n a -> Bool

    isElemF x [] = False

    isElemF x (y :: xs) = False

  • Beweis als Objekt data Position : a -> Vect n a -> Type where

    Head : Position x (x::xs)

    Tail : Position x xs -> Position x (y::xs)

  • Beispiele oneInVector : Position 1 [1, 2, 3]

    oneInVector = Head

    twoInVector : Position 2 [1, 2, 3]

    twoInVector = Tail Head

    -- fourInVector : Position 4 [1, 2, 3]

    -- fourInVector = Tail (Tail (Tail ?fourInVector_rhs1))

  • Elemente gleich? data Equals : a -> a -> Type where

    Same : Equals x x

    maybeEq : (x : a) -> (y: a) -> Maybe (Equals x y)

    data Maybe : a -> Type where

    Nothing : Maybe a

    Just : a -> Maybe a

  • Element-Test mit Beweis isElem : Eq a =>

    (x : a) -> (xs : Vect n a) -> Maybe (Position x xs)

    isElem x [] = Nothing

    isElem x (y :: xs) = case maybeEq x y of

    Nothing => (case isElem x xs of

    Nothing => Nothing

    (Just pos) => Just (Tail pos))

    (Just Same) => Just Head

  • http://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris.pdf

  • https://sel4.systems/

  • http://www.russinoff.com/papers/paris.ps

  • Dokumentation Spezifikation

    Typen

    Verifikation Generierung

  • Tools • Coq • Isabelle • Agda • Idris • ATS • F* • ACL2 • Liquid/Dependent Haskell

  • Auf dem Weg ...

  • http://flint.cs.yale.edu/certikos/

  • Code vs. Dokumentation

    "A program, written without requirements and specifications, can never be incorrect - it can only be surprising."

    Young, Boebeit, and Kainin: "Proving a Computer System Secure", The Scientific Honeyweller, Vol. 6, Nr. 2 (Juli 1985)