Objektorientierte und funktionale SoftwareentwicklungRefactoring von Java Legacy CodeClean Code und Software CraftsmanshipSpecification by Example und

Domain-Driven DesignFacilitation 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

Listendata List: (a:Type) -> Type where

Nil : List a

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

ListenmapL : (a -> b) -> List a -> List b

mapL f [] = []

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

Nicht-Terminationx : a

x = x

Vektorendata Vect : (n:Nat) -> (a:Type) -> Type where

Nil: Vect 0 a

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

Automatische Herleitung ImplementierungmapV : (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 Objektdata Position : a -> Vect n a -> Type where

Head : Position x (x::xs)

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

BeispieleoneInVector : 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 BeweisisElem : 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

DokumentationSpezifikation

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)