|
|
Executing JML Specifications via Constraint Programming
Dr. Tim Wahls
Friday, April 18, 2008
10:30AM ~ 11:30AM, Harris Center 101
Abstract
Formal specifications are more useful and easier to develop if they
are executable. We describe a system for executing specifications
written in the Java Modeling Language (JML) by translating them to
constraint programs, which are then executed via the Java Constraint
Kit (JCK). Our system can execute specifications written at a high
level of abstraction, and the generated constraint programs are Java
implementations of the translated specifications. Hence, they can be
called directly from ordinary Java code.
Short Bio
Tim Wahls is an Associate Professor of Computer Science at Dickinson
College in Carlisle, Pennsylvania. His research interests include the
role of formal methods in software development, with a particular
emphasis on executing formal specifications using constraint logic
programming techniques. He has also published several papers in the
area of computer science education. His teaching specializations are
programming languages and software engineering.
|
|