Nächster Vortrag: Design by Contract with JML (Joe Kiniry) am 22.09. | Print |
Written by Michael Jastram   
Tuesday, 29 June 2010 07:52

Der Vortrag

The idea of Design by Contract, or DBC for short, is that one should precisely, but not completely, describe a software system before it is built.  The descriptions are called contracts.  Programming contracts are like legal contracts that describe a business deal, as they describe a relationship between parties and each parties' responsibility to the other, expect the "parties" are programs and the "deal" is a system design.

DBC, as applied to OO software, is the brainchild of Meyer, and was originally realized in an elegant form in the Eiffel programming language.  The facets that make up a contract, assertions in the form of preconditions and postconditions, and well-formedness conditions on types, object, classes, and their ilk, harked back to the grandfathers of formal methods: Floyd, Hoare, Dijkstra, and others.

DBC has found its way into the mainstream of programming via some unlikely supporters.  Microsoft has been using lightweight contracts for over a decade in the form of ACSL specifications, and several tools included with Visual Studio and available from Microsoft Research use contracts for a variety of purposes, from lightweight static analysis, runtime checking, and test generation for C#, to full functional verification of C programs.

In the Open Source world, DBC specification languages and frameworks are available the vast majority of programming languages in use today.  The richest of these, both in terms of language expressiveness and tool support, is the Java Modeling Language (JML).  Using JML, which essentially looks and smells like Java, one can precisely describe the properties of a Java system, either one that you intend to build (and thus you are practicing Design by Contract) or one that have already built (and thus you are Contracting the Design, as we put it).

Dozens of tools understand JML, including documentation and test case generators, runtime checkers, model checkers, verification systems, and more.  In this talk I will summarize the JML language, review the current state of tool support and demonstrate some tools, and highlight some best practices and case studies from academia and industry.

Der Sprecher

Joseph Kiniry started his first company while in his early twenties and has since founded five technology firms. In addition, he has also has helped get another half dozen companies off the ground by providing business, technical, and managerial advice. For the past decade, Joe has been an independent consultant in, among other things, formal methods, distributed systems, software engineering, Internet security and computer graphics. Joe earned a Ph.D. from the the California Institute of Technology. He leads the KindSoftware: Software Engineering with Applied Formal Methods research group and was a co-founder of the Systems Research Group at UCD. Currently Joe is anan Associate Professor in the Software Development Group at the IT University of Copenhagen.

Poster zum Vortrag

Unser Sponsor: Raytion

Wir freuen uns, bereits zum zweiten Mal Raytion als Sponsor gewonnen zu haben.

Raytion ist ein unabhängiges, weltweit tätiges Unternehmen im Bereich IT-Beratung und Softwareentwicklung. Zur Unterstützung der Teams in Düsseldorf und Hamm ist Raytion auf der Suche nach engagierten Projektleitern und Softwarearchitekten/Softwareentwicklern.

Wann und wo?

Die Veranstaltung findet am Mittwoch, den 22.09 statt, wie immer im Hörsaal 5F der Düsseldorf Heinrich-Heine-Universität. Eintritt, Essen und Getränke frei...