Dozenten: Markus Rentschler Andreas Stuckert Skript zur Vorlesung Software Engineering I VE 13:...

Dozenten:Markus RentschlerAndreas Stuckert

Skript zur Vorlesung

Software Engineering I

VE 13: Logische Basiskonzepte I




• Einführung• Syllogismen• Formale Logik

– Aussagenlogik– Prädikatenlogik– Temporale Logik

• OCL• Entscheidungstabellen (VE 14)• Regeln (VE 14)

Agenda

Version: 04/26/23 2Software Engineering I VE 13: Logische Basiskonzepte




Basiskonzepte


Beschreiben das Verhalten und die

Veränderungen während der Laufzeit.

Beschreiben die feste Struktur des Systems, die sich während der Laufzeit nicht ändert.

Beschreiben die Programmfunktion

logisch und mathematisch




Überblick

Version 04/26/23 4

Weitgehend sind für uns die Bereiche der formalen Logik wichtig Aussagelogik und Prädikatenlogik

Software Engineering I VE 13: Logische Basiskonzepte





Ein Zitat von Edsger W. Dijkstra:Informatik = VLSAL (Very large scale application of logics)




Syllogismen





Syllogismen


• syllogismos = das Zusammenrechnen, logischer Schluss, folgern• Katalog von Typen logischer Argumente • Kern der antiken Logik des Aristoteles (400 bc) und der traditionellen Logik (1900)

A syllogism is discourse in which, certain things being stated, something other than what is stated follows of necessity from their being so.

(from The Complete Works of Aristotle)

• Syllogismen sind immer nach dem gleichen Muster aufgebaut. • Jeweils zwei Prämissen, Obersatz und Untersatz genannt, führen zu einer

Konklusion. Die Prämissen und die Konklusion sind Aussagen von einem bestimmten Typ, in denen jeweils einem Begriff, dem syllogistischen Subjekt, ein anderer Begriff, das syllogistische Prädikat, in bestimmter Weise zu- oder abgesprochen wird.

• In Abhängigkeit von der Stelle, an der sie im Syllogismus auftreten, werden die vorkommenden Begriffe Oberbegriff, Mittelbegriff und Unterbegriff genannt.




• Hieraus ergeben sich sogenannte Figuren• durch Kombination ergeben sich 256 mögliche

Kombinationen, von denen 24 gültige Aussagen darstellen

• Diese werden traditionell mit Merkwörtern bezeichnet• man unterscheidet zwischen schwachen und starken

Folgerungen

Syllogismen


1. Figur 2. Figur 3. Figur 4. Figur

erste Prämisse M – P P – M M – P P – M

zweite Prämisse S – M S – M M – S M – S

Konklusion S – P S – P S – P S – P

1. Figur: Barbara, Celarent, Darii, Ferio, Barbari, Celaront

2. Figur: Baroco, Cesare, Camestres, Festino, Camestrop, Cesaro

3. Figur: Bocardo, Darapti, Datisi, Disamis, Felapton, Ferison

4. Figur: Bamalip, Calemes, Dimatis, Fesapo, Fresison, Calemop




• Modus Barbara (stark): Alle Münchner sind Bayern, alle Schwabinger sind Münchner. Es folgt: Alle Schwabinger sind Bayern.

• Modus Barbari (schwach): Alle Münchner sind Bayern, alle Schwabinger sind Münchner. Es folgt: Einige Schwabinger sind Bayern.

• Modus Celarent (stark): Kein Münchner ist Passauer, alle Schwabinger sind Münchner, es folgt: Kein Schwabinger ist Passauer.

• Modus Celaront (schwach): Kein Münchner ist Passauer, alle Schwabinger sind Münchner. Es folgt: Einige Schwabinger sind keine Passauer.

Syllogismen (Beispiele)





• sie liefern die Grundlage für die moderne Logik

• eignen sich zum Hierarchisieren und Strukturieren von Argumenten

• lassen sich leicht formulieren und ausdrücken• können durch Kombination und

Formalisierung für das Entwerfen von regelbasierter Systeme verwendet werden

Syllogismen





• zur Beschreibung von Logik bedient man sich formalisierter Syntax und Semantik

Probleme mit natürlicher Sprache


Warum?• Zuordnung von Wahrheitswerten zu natursprachlichen Aussagen ist

problematisch• Natürliche Sprache ist oft schwer verständlich („analytika priora“

von Aristoteles)• Natürliche Sprache ist mehrdeutig

Ich sah den Mann auf dem Berg mit dem Fernrohr.








Aussagenlogik





Aussagenlogik


Vertiefung in einer bereits stattgefundenen Vorlesung




Prädikatenlogik


Vertiefung in einer bereits stattgefundenen Vorlesung




• Baut auf der Aussage und Prädikantenlogik auf• Drei maßgebliche Zweige

– LTL (Lineare temporale Logik) beschreibt Abfolgen– CTL (Computation Tree Logic) beschreibt verzweigte

Systeme– CTL* (Mischung aus LTL und CTL)

• Hat neben dem statischen Verhalten auch einen Zeitbegriff. Dieser ist aber nicht physikalisch als Zeit zu verstehen, sondern als Kausalitätsreihenfolge.

• Einführung von temporalen Operatoren– X im nächsten Schritt– F irgendwann– G immer– U so lange, bis …

Temporale Logik





• Krippe-StrukturBeispiel Temporale Logik


Immer, wenn die Tür geschlossen wird und auf Start gedrückt wird, kann das Essen erhitzt werden.

Immer, wenn die Tür nicht geschlossen ist und auf Start gedrückt wird, kann das Essen nicht erhitzt werden oder die Mikrowelle wird eventuell zurückgesetzt.




• Sie verknüpfen logische Bedingungen (Einschränkungen, Zusicherung) mit Inhalten, Zuständen und semantischen Formulierungen

• Spezifikation von Invarianten in der OO• Bedingungen in Sequenzdiagrammen• Vor und Nachbedingungen für Methoden (pre, post) • Guards bei Zustandsdiagrammen• Contraints immer im Rahmen eines Kontextes

Constraints





Constraints





OCL


• Object Constraints Language – Object steht hier für eine Komponente eines beliebigen

Systems, diese soll genauer spezifiziert, definiert oder beschrieben werden.

– Language steht hier nicht für eine formale Computersprache, sondern vielmehr für eine auf jede Implementierung anwendbare, weniger formale Sprache.

• Ergänzung zu UML um Modellierung noch effizienter zu gestalten (also kein eigener Diagrammtyp)

• Sie verändern ein Model nicht, sie überwachen es • OCL alleine ist ungeeignet zur Modellierung




1. Das Alter einer Person ist nicht negativ.2. Eine Person ist jünger als ihre Eltern.3. Nach einem Geburtstag ist eine Person um genau 1 Jahr älter.4. Eine Person hat genau 2 Eltern.5. Wenn jemand ein Kind bekommen hat, ist die Menge seiner

Kinder nicht leer und die Anzahl seiner Kinder ist größer als vorher.6. Nur eine erwachsene Person darf ein Auto besitzen.7. Die Erstzulassung eines Autos liegt nicht vor dem Baujahr.8. Jede Person, die mindestens ein Auto besitzt, hat mindestens ein

Auto, das jünger ist als sie selbst.9. Niemand kann von sich selbst ein Elternteil sein.10. Es gibt mindestens eine Person, die ein Auto besitzt (bzw. von

allen Personen gibt es mindestens eine Person, die mindestens ein Auto besitzt).

Beispiel OCL Text





OCL Klassendiagramm





1. context Person inv: self.Alter >=02. context Person inv: self.Eltern->forAll(e|e.Alter>self.Alter)3. context Person::hatGeburtstag() post: self.Alter=self.Alter@pre+14. context Person inv: self.Eltern->size()=25. context Person::bekommtKind() post: self.Kinder->notEmpty() and

self.Kinder->size() > self.Kinder@PRE->size()6. context Person inv: self.Alter<18 implies autos->size()=07. context Auto inv: self.Erstzulassung>=self.Baujahr8. context Person inv: self.autos->size()>0 implies self.autos-

>exists( a | Calendar.YEAR - a.baujahr < self.alter)9. context Person inv: not self.eltern->includes(self)10. context Person inv: Person.allInstances->exists(p | p.autos->size()

> 0

OCL Constraints


Weiteres Beispiel und Operantenübersicht: Balzert Seite 382 - 385




• Formale Logik … – hilft uns, Programme eindeutig und präzise zu

beschreiben– basiert auf den mathematischen Grundsätzen der

boolschen Algebra und der Mengenlehre– kann Wahrheitsaussagen, Beziehungen von

Objekten und zeitliche Abfolgen beschreiben• OCLs erweitern die bestehenden UML

Diagramme um eine Beschreibung für die Beschaffenheit und Grenzen von Objekten

Zusammenfassung

Version 04/26/23 24




Fragen?





1. Modellieren Sie ein Code-Schloss, das mit einer Ziffern-Tastatur bedient wird. Um das Schloss zu öffnen, müssen drei Ziffern in korrekter Reihenfolge eingegeben werden. Zeichnen Sie a ein Zustandsdiagramm und b eine Zustandstabelle des entsprechenden Mealy-Automaten.

2. Entwickeln Sie eine Stoppuhr für den Sportbereich, die folgende Eigenschaften besitzt:1. Die Stoppuhr kann ein- und ausgeschaltet werden.2. Die Stoppuhr kann gestartet und gestoppt werden. Nach dem Stopp wird die vergangene Zeit

zwischen Start und Stopp angezeigt.3. Nach dem Start kann eine Zwischenzeit angezeigt werden. Die Uhr läuft im Hintergrund weiter. Nun

kann entweder die Anzeige von der Zwischenzeit auf die Anzeige der aktuell verbrauchten Gesamtzeit gewechselt werden oder die im Hintergrund laufende Uhr kann angehalten werden, ohne dass sich die Anzeige ändert. Im letzten Fall wird nach einem weiteren Knopfdruck die vergangene Gesamtzeit angezeigt.

4. Die zwischen Start und Stopp vergangene Zeit kann bei stehender Uhr und Anzeige der vergangenen Gesamtzeit auf Null zurückgesetzt werden.

5. Die Uhr besitzt zwei Druckknöpfe (die nicht gleichzeitig gedrückt werden können).

a. Zeichnen Sie das Zustandsübergangsdiagramm eines Mealy-Automaten für die oben beschriebene Stoppuhr.

b. Integrieren Sie den Automaten für die Normalzeit und den Automaten für die Stoppuhr zu einem hierarchischen Automatenmodell einer digitalen Armbanduhr mit drei Druckknöpfen.

Übung


Date post:	06-Apr-2016
Category:	Documents
Upload:	roland-guenther
View:	238 times
Download:	4 times

Dozenten: Markus Rentschler Andreas Stuckert Skript zur Vorlesung Software Engineering I VE 13:...

Documents