Download - Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

Transcript
Page 1: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

Page 2: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

Michael Sperber

• funktionale Programmierung

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

• Schulungen und Coaching

• Blog: funktionale-programmierung.de

• Entwickerkonferenz BOB bobkonf.de

Page 3: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design
Page 4: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design
Page 5: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

"IoT Goes Nuclear:Creating a ZigBee Chain Reaction"

http://iotworm.eyalro.net/

Page 6: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

Page 7: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

http://heartbleed.com/

Page 8: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

Page 9: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

Page 10: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

FIXME

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

Page 11: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design
Page 12: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

Korrekte Software – wie?

Page 13: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

Intel Pentium, FDIV-Bug

Page 14: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

Nil : List a

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

Page 15: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

mapL f [] = []

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

Page 16: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

Nicht-Terminationx : a

x = x

Page 17: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

Nil: Vect 0 a

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

Page 18: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

Automatische Herleitung ImplementierungmapV : (a-> b) -> Vect n a -> Vect n b

mapV f [] = []

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

Page 19: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

isElemF x [] = False

isElemF x (y :: xs) = False

Page 20: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

Beweis als Objektdata Position : a -> Vect n a -> Type where

Head : Position x (x::xs)

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

Page 21: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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))

Page 22: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

Page 23: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

Page 24: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design
Page 25: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design
Page 26: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

Page 27: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

https://sel4.systems/

Page 28: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

Page 29: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

DokumentationSpezifikation

Typen

Verifikation Generierung

Page 30: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

Page 31: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

Auf dem Weg ...

Page 32: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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

Page 33: Objektorientierte und funktionale Softwareentwicklung ... · Refactoring von Java Legacy Code Clean Code und Software Craftsmanship Specification by Example und Domain-Driven Design

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)