********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle W, 4e`me e'tage, toits du DMI * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 4 avril 1997 **** 14h00 ******************************** Inference de type recursive polymorphe bornee en ML< Alexandre FREY (ENSMP) Re'sume' : non parvenu. *** Vendredi 11 avril 1997 **** 14h00 ******************************* Rela^che. *** Vendredi 18 avril 1997 **** 14h00 ******************************* Extended Static Checking K. Rustan M. LEINO (Digital Equipment Corporation, Systems Research Center) Re'sume' : The Extended Static Checker (ESC) is a programming tool that works on object-oriented, concurrent programs to find programming errors like nil-dereference errors, array index out-of-bounds errors, deadlocks, and race conditions. To use the tool, a programmer annotates a program with simple specifications. ESC works by transforming a program and its specifications into verification conditions (logical formulas) that are passed to an automatic theorem prover. ESC has been applied to, for example, Modula-3's object-oriented I/O streams library. In this talk, I will give an overview and a demo of the ESC system. *** Vendredi 25 avril 1997 **** 14h00 ******************************* Static verification of integrity constraints in object-oriented database programming languages via predicate transformers. Ve'ronique BENZAKEN (Universite de Paris I - Pantheon - Sorbonne & L.R.I, Universite de Paris XI) Re'sume' : We propose a technique to statically manage integrity constraints in object-oriented database programming languages. Integrity constraints are statements which restrict the possible (coherent) states of a database. We place ourselves in the context of a simplified database programming language, close to O$_2$, in which we assume that updates are undertaken by means of methods. An important issue when dealing with constraints is that of efficiency. A naive management of such constraints can cause a severe floundering of the overall system. Our basic assumption is that the run-time checking of constraints is too costly to be undertaken systematically. Therefore, methods that are always safe with respect to integrity constraints should be proven so {\em at compile time}. The run-time checks should only concern the remaining methods. To that purpose, we propose a new approach, based on the use of predicate transformers, to prove the {\em invariance} of {\em integrity constraints} under complex {\em methods}. We then describe the current implementation of our prototype, and report some experiments that have been performed with it on non trivial examples. The counterpart of the problem of program verification is that of program correction. Static analysis techniques can also be applied to solve that problem. We present a systematic approach to undertake the automatic correction of unsafe methods. However, the advantages of the latter technique are not as clear as those of program verification. We will therefore discuss some arguments for and against the use of method correction. Though our work is developed in the context of object-oriented database programming languages, it can easily be applied to the problem of static verification and correction of object-oriented languages providing pre and post-conditions such as Eiffel. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr WWW: http://www.ens.fr/~cousot/annonceseminaire.html *********************************************************************