@phdthesis{Sekerinski94VerfeinerungOOP,
	type = {Dissertation},
	title = {Verfeinerung in der {Objektorientierten} {Programmkonstruktion}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski94VerfeinerungOOP.pdf},
	abstract = {Die vorliegende Arbeit gibt eine formale Fundierung objektorientierter Entwurfsprinzipien. Hierzu wird eine Notation definiert, die zum einen alle wesentlichen Elemente objektorientierter Programmiersprachen enthält, und zum anderen Spezifikationskonstrukte bietet. In dieser Notation werden folgende typische objektorientierte Entwurfsprinzipien betrachtet:
• Implementieren von Klassen
• Inkrementelles Modifizieren von Klassen durch Vererbung
• Herausfaktorisieren von Gemeinsamkeiten von Klassen
Es werden Beweis- und Konstruktionsregeln für die korrekte Anwendung dieser Entwurfsprinzipien aufgestellt. Die Regeln tragen auch zu einem tieferen Verständnis der Entwurfsprinzipien bei.
Spezifikationen haben die Form von indeterministischen Anweisungen, wie sie
aus dem Verfeinerungskalkül bekannt sind, bei denen das Resultat durch ein
Prädikat spezifiziert wird. An objektorientierten Konzepten werden Objekte mit
Attributen und Methoden, Kapselung privater Attribute, Klassen mit Vererbung,
Untertyp-Polymorphie, parametrische Polymorphie und Objektidentitäten betrachtet. Für die Semantik der Notation wird das Typsystem Fω≤, eine Erweiterung des typisierten λ-Kalküls, zugrunde gelegt. Anweisungen werden durch Prädikatentransformer definiert. Damit wird gezeigt, wie eine Notation, die bezüglich der Spezifikationsmächtigkeit und der Flexibilität der Typisierung über existierende typisierte objektorientierte Programmier- und Spezifikationssprachen hinausgeht, formal definiert werden kann. Die Flexibilität beruht insbesondere auf der Unterscheidung von Objekttypen und Klassen.
Das zentrale methodische Konzept ist die Klassenverfeinerung. Sie erlaubt es, abstrakte, spezifizierende Klassen durch konkretere, implementierungsnähere zu ersetzen. Es wird gezeigt, daß Klassenverfeinerung durch die aus dem Verfeinerungskalkül bekannte Technik der Datenverfeinerung nachgewiesen werden kann. Für die Verfeinerung von inkrementell modifizierten Klassen werden spezielle, vereinfachte Beweisregeln aufgestellt. Das Herausfaktorisieren von Gemeinsamkeiten von Klassen wird durch zwei neuartige Operatoren, Klassenschnitt und Klassenvereinigung, unterstützt.},
	school = {University of Karlsruhe},
	author = {Sekerinski, Emil},
	year = {1994},
}

{"_id":"KGnttLCg2eoF84axx","bibbaseid":"sekerinski-verfeinerunginderobjektorientiertenprogrammkonstruktion-1994","downloads":0,"creationDate":"2019-02-02T15:48:53.614Z","title":"Verfeinerung in der Objektorientierten Programmkonstruktion","author_short":["Sekerinski, E."],"year":1994,"bibtype":"phdthesis","biburl":"https://api.krunk.cn/emil/bib.php","bibdata":{"bibtype":"phdthesis","type":"Dissertation","title":"Verfeinerung in der Objektorientierten Programmkonstruktion","url":"https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski94VerfeinerungOOP.pdf","abstract":"Die vorliegende Arbeit gibt eine formale Fundierung objektorientierter Entwurfsprinzipien. Hierzu wird eine Notation definiert, die zum einen alle wesentlichen Elemente objektorientierter Programmiersprachen enthält, und zum anderen Spezifikationskonstrukte bietet. In dieser Notation werden folgende typische objektorientierte Entwurfsprinzipien betrachtet: • Implementieren von Klassen • Inkrementelles Modifizieren von Klassen durch Vererbung • Herausfaktorisieren von Gemeinsamkeiten von Klassen Es werden Beweis- und Konstruktionsregeln für die korrekte Anwendung dieser Entwurfsprinzipien aufgestellt. Die Regeln tragen auch zu einem tieferen Verständnis der Entwurfsprinzipien bei. Spezifikationen haben die Form von indeterministischen Anweisungen, wie sie aus dem Verfeinerungskalkül bekannt sind, bei denen das Resultat durch ein Prädikat spezifiziert wird. An objektorientierten Konzepten werden Objekte mit Attributen und Methoden, Kapselung privater Attribute, Klassen mit Vererbung, Untertyp-Polymorphie, parametrische Polymorphie und Objektidentitäten betrachtet. Für die Semantik der Notation wird das Typsystem Fω≤, eine Erweiterung des typisierten λ-Kalküls, zugrunde gelegt. Anweisungen werden durch Prädikatentransformer definiert. Damit wird gezeigt, wie eine Notation, die bezüglich der Spezifikationsmächtigkeit und der Flexibilität der Typisierung über existierende typisierte objektorientierte Programmier- und Spezifikationssprachen hinausgeht, formal definiert werden kann. Die Flexibilität beruht insbesondere auf der Unterscheidung von Objekttypen und Klassen. Das zentrale methodische Konzept ist die Klassenverfeinerung. Sie erlaubt es, abstrakte, spezifizierende Klassen durch konkretere, implementierungsnähere zu ersetzen. Es wird gezeigt, daß Klassenverfeinerung durch die aus dem Verfeinerungskalkül bekannte Technik der Datenverfeinerung nachgewiesen werden kann. Für die Verfeinerung von inkrementell modifizierten Klassen werden spezielle, vereinfachte Beweisregeln aufgestellt. Das Herausfaktorisieren von Gemeinsamkeiten von Klassen wird durch zwei neuartige Operatoren, Klassenschnitt und Klassenvereinigung, unterstützt.","school":"University of Karlsruhe","author":[{"propositions":[],"lastnames":["Sekerinski"],"firstnames":["Emil"],"suffixes":[]}],"year":"1994","bibtex":"@phdthesis{Sekerinski94VerfeinerungOOP,\n\ttype = {Dissertation},\n\ttitle = {Verfeinerung in der {Objektorientierten} {Programmkonstruktion}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski94VerfeinerungOOP.pdf},\n\tabstract = {Die vorliegende Arbeit gibt eine formale Fundierung objektorientierter Entwurfsprinzipien. Hierzu wird eine Notation definiert, die zum einen alle wesentlichen Elemente objektorientierter Programmiersprachen enthält, und zum anderen Spezifikationskonstrukte bietet. In dieser Notation werden folgende typische objektorientierte Entwurfsprinzipien betrachtet:\n• Implementieren von Klassen\n• Inkrementelles Modifizieren von Klassen durch Vererbung\n• Herausfaktorisieren von Gemeinsamkeiten von Klassen\nEs werden Beweis- und Konstruktionsregeln für die korrekte Anwendung dieser Entwurfsprinzipien aufgestellt. Die Regeln tragen auch zu einem tieferen Verständnis der Entwurfsprinzipien bei.\nSpezifikationen haben die Form von indeterministischen Anweisungen, wie sie\naus dem Verfeinerungskalkül bekannt sind, bei denen das Resultat durch ein\nPrädikat spezifiziert wird. An objektorientierten Konzepten werden Objekte mit\nAttributen und Methoden, Kapselung privater Attribute, Klassen mit Vererbung,\nUntertyp-Polymorphie, parametrische Polymorphie und Objektidentitäten betrachtet. Für die Semantik der Notation wird das Typsystem Fω≤, eine Erweiterung des typisierten λ-Kalküls, zugrunde gelegt. Anweisungen werden durch Prädikatentransformer definiert. Damit wird gezeigt, wie eine Notation, die bezüglich der Spezifikationsmächtigkeit und der Flexibilität der Typisierung über existierende typisierte objektorientierte Programmier- und Spezifikationssprachen hinausgeht, formal definiert werden kann. Die Flexibilität beruht insbesondere auf der Unterscheidung von Objekttypen und Klassen.\nDas zentrale methodische Konzept ist die Klassenverfeinerung. Sie erlaubt es, abstrakte, spezifizierende Klassen durch konkretere, implementierungsnähere zu ersetzen. Es wird gezeigt, daß Klassenverfeinerung durch die aus dem Verfeinerungskalkül bekannte Technik der Datenverfeinerung nachgewiesen werden kann. Für die Verfeinerung von inkrementell modifizierten Klassen werden spezielle, vereinfachte Beweisregeln aufgestellt. Das Herausfaktorisieren von Gemeinsamkeiten von Klassen wird durch zwei neuartige Operatoren, Klassenschnitt und Klassenvereinigung, unterstützt.},\n\tschool = {University of Karlsruhe},\n\tauthor = {Sekerinski, Emil},\n\tyear = {1994},\n}\n\n","author_short":["Sekerinski, E."],"key":"Sekerinski94VerfeinerungOOP","id":"Sekerinski94VerfeinerungOOP","bibbaseid":"sekerinski-verfeinerunginderobjektorientiertenprogrammkonstruktion-1994","role":"author","urls":{"Paper":"https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski94VerfeinerungOOP.pdf"},"metadata":{"authorlinks":{}},"downloads":0},"search_terms":["verfeinerung","der","objektorientierten","programmkonstruktion","sekerinski"],"keywords":[],"authorIDs":[],"dataSources":["fDYYrPxpzcyDvQK6b","pKojZwgcmAbzT5ufq","So4gmSWFmbQRNEuFs","HEdahWqKBpmSGmDwq","yBNL6zg4bd77wFNse","CvQYP6Tmpapx74Mgr","RWydLHbBJqgdeh5jr"]}