1. D. Le Métayer, V.-A. Nicolas, and O. Ridoux. Programs, Properties, and Data: Exploring the Software Development Trilogy. IEEE Software, 15(6):75-81, November/December 1998. [WWW] Keyword(s): Software engineering, testing, verification, program analysis, program learning. Abstract:

   Software development usually involves a collection of properties, programs and data as input or output documents. Putting these three kinds of documents at the vertices of a triangle, one sees that all three sides of the triangle have been exploited in formal methods, and that they have often been used in both directions. However, richer combinations have seldom been envisaged, and formal methods often amount to a strict orientation of the figure by imposing functional dependencies (e.g.,~infering test cases from specifications). Moreover, undecidability problems arise when properties are expressed in full predicate logic (or similar formalisms) or programs are written in Turing-equivalent programming languages. We advocate that (1) formal methods should provide more flexible ways to exploit the developer's knowledge and offer a variety of possibilities to construct programs, properties and test data and (2) it is worth restricting the power of logic formalisms and programming languages for the benefit of mechanization. We go one step in this direction, and present a formal method for generating test cases that combines techniques from abstract interpretation ({\em program -> property}) and testing ({\em program+property -> test data}), and takes inspiration from automated learning (test generation via a {\em testing bias}). The crucial property of the test suites generated this way is that they are robust with respect to a test objective formalized as a property. In other words, if a program passes the test suite, then it is guaranteed to satisfy the property. As this process leads to decision problems in very restricted formalisms, it can be fully mechanized.

   
   

   @Article{dlm-van-or-IEEEsoftware98,
   author = {D. Le~Métayer and V.-A. Nicolas and O. Ridoux},
   title = {Programs, Properties, and Data: Exploring the Software Development Trilogy},
   journal = {IEEE Software},
   pages = {75-81},
   volume = {15},
   number = {6},
   month = {November/December},
   year = {1998},
   url = {http://www.irisa.fr/lande/vnicolas/articleIEEE98.pdf},
   keywords = {Software engineering, testing, verification, program analysis, program learning},
   abstract = {Software development usually involves a collection of properties, programs and data as input or output documents. Putting these three kinds of documents at the vertices of a triangle, one sees that all three sides of the triangle have been exploited in formal methods, and that they have often been used in both directions. However, richer combinations have seldom been envisaged, and formal methods often amount to a strict orientation of the figure by imposing functional dependencies (e.g.,~infering test cases from specifications). Moreover, undecidability problems arise when properties are expressed in full predicate logic (or similar formalisms) or programs are written in Turing-equivalent programming languages. We advocate that (1) formal methods should provide more flexible ways to exploit the developer's knowledge and offer a variety of possibilities to construct programs, properties and test data and (2) it is worth restricting the power of logic formalisms and programming languages for the benefit of mechanization. We go one step in this direction, and present a formal method for generating test cases that combines techniques from abstract interpretation ({\em program -> property}) and testing ({\em program+property -> test data}), and takes inspiration from automated learning (test generation via a {\em testing bias}). The crucial property of the test suites generated this way is that they are robust with respect to a test objective formalized as a property. In other words, if a program passes the test suite, then it is guaranteed to satisfy the property. As this process leads to decision problems in very restricted formalisms, it can be fully mechanized.} 
   }
   

1. M. Ducassé. Teaching B at a Technical University is Possible and Rewarding. In H. Habrias and S. E. Dunn, editors, B'98, Proceedings of the Educational Session, avril 1998. Association de Pilotage des Conférences B, Nantes. Note: ISBN: 2-9512461-0-2. [WWW] Keyword(s): B formal method, teaching. Abstract:

   In January 1994, to replace a highly unpopular denotational semantics course, I undertook to set up a course on the B method at the INSA of Rennes (Institut National des Sciences Appliquées), at a Bac+4 level. I had almost no previous knowledge of formal methods. I had, however, programmed much in Prolog and felt the need for a strong programming discipline, supported if possible by methods and tools. The experience is, in my opinion, successful. The students do learn much during the course, find interesting placements where their competence is appreciated and every occurrence of the course teaches me something. In the article, I first list reasons to start the experience. I then discuss the pedagogical objectives of the course. The contents of the course is given and an assessment is made.

   
   

   @InProceedings{ducasse98c,
   Author={M. Ducassé},
   url={http://www.irisa.fr/lande/ducasse/B-edu-98.ps.gz},
   Title={Teaching B at a Technical University is Possible and Rewarding},
   BookTitle={B'98, Proceedings of the Educational Session},
   Year={1998},
   Editor={H. Habrias and S. E. Dunn},
   Publisher={Association de Pilotage des Conférences B, Nantes},
   Month={avril},
   Note={ISBN: 2-9512461-0-2},
   keywords={B formal method, teaching},
   abstract={In January 1994, to replace a highly unpopular denotational semantics course, I undertook to set up a course on the B method at the INSA of Rennes (Institut National des Sciences Appliquées), at a Bac+4 level. I had almost no previous knowledge of formal methods. I had, however, programmed much in Prolog and felt the need for a strong programming discipline, supported if possible by methods and tools. The experience is, in my opinion, successful. The students do learn much during the course, find interesting placements where their competence is appreciated and every occurrence of the course teaches me something. In the article, I first list reasons to start the experience. I then discuss the pedagogical objectives of the course. The contents of the course is given and an assessment is made.}
   }
   




2. M. Ducassé and J. Noyé. Tracing Prolog Programs by Source Instrumentation is Efficient Enough. In K. Sagonas, editor, IJCSLP'98 Post-conference workshop on Implementation Technologies for Programming Languages based on Logic., June 1998. [WWW] Keyword(s): Debugging, tracing, source to source transformation, benchmarking, Prolog. Abstract:

   Tracing by automatic program source instrumentation has major advantages over compiled code instrumentation: it is more portable, it benefits from many compiler optimizations, it produces traces in terms of the original program, and it can be tailored to specific debugging needs. The usual argument in favor of compiled code instrumentation is its supposed efficiency. We have compared the performance of two operational low-level Prolog tracers with source instrumentation. We have executed classical Prolog benchmark programs, collecting trace information without displaying it. On average, collecting trace information by program instrumentation is about as fast as using a low-level tracer in one case, and only twice slower in the other. This is a minor penalty to pay, compared to the advantages of the approach. To our knowledge, this is the first time that a quantitative comparison of both approaches is made for any programming language.

   
   

   @InProceedings{ducasse98b,
   Author={M. Ducassé and J. Noyé},
   url={http://www.irisa.fr/lande/ducasse/ducasse-noye-manchester-98.ps.gz},
   Title={Tracing {Prolog} Programs by Source Instrumentation is Efficient Enough},
   BookTitle={IJCSLP'98 Post-conference workshop on Implementation Technologies for Programming Languages based on Logic.},
   Year={1998},
   Editor={K. Sagonas},
   Month={June},
   keywords={Debugging, tracing, source to source transformation, benchmarking, Prolog},
   abstract={Tracing by automatic program source instrumentation has major advantages over compiled code instrumentation: it is more portable, it benefits from many compiler optimizations, it produces traces in terms of the original program, and it can be tailored to specific debugging needs. The usual argument in favor of compiled code instrumentation is its supposed efficiency. We have compared the performance of two operational low-level Prolog tracers with source instrumentation. We have executed classical Prolog benchmark programs, collecting trace information without displaying it. On average, collecting trace information by program instrumentation is about as fast as using a low-level tracer in one case, and only twice slower in the other. This is a minor penalty to pay, compared to the advantages of the approach. To our knowledge, this is the first time that a quantitative comparison of both approaches is made for any programming language. }
   }
   




3. S. Mallet and M. Ducassé. Pilotage d'un méta-interprète ensembliste par une trace ``relationnelle'' pour le débogage de bases de données déductives. In O. Ridoux, editor, Journées francophones de Programmation Logique et programmation par Contraintes, Nantes, pages 151-165, mai 1998. JFPLC'98, Hermes. [WWW] Keyword(s): bases de données déductives, débogage, trace, sémantique opérationnelle, multi-SLD-AL, méta-interprète, ensembles de substitutions, instrumentation. Abstract:

   Le développement des bases de données déductives nécessite des outils, en particulier pour le débogage. Les bases de données déductives gèrent des quantités importantes de données et, en général, de manière ensembliste. Les systèmes d'explication existants pour les bases de données déductives ne prennent pas en compte ces contraintes. Nous proposons une technique de traçage qui consiste à intégrer une trace ``relationnelle'' avec un méta-interprète instrumenté utilisant des ensembles de substitutions. La trace relationnelle donne, de manière efficace, de l'information précise sur l'extraction de données de la base relationnelle. Le méta-interprète ensembliste gère des ensembles de substitutions et donne des explications sur la déduction. Les aspects coûteux de la méta-interprétation sont réduits par l'utilisation de la trace qui évite beaucoup de calculs. La flexibilité de la méta-interprétation est conservée. Elle permet de produire facilement des traces de profils différents.

   
   

   @InProceedings{mallet98a,
   author = "S. Mallet and M. Ducassé",
   title = "Pilotage d'un méta-interprète ensembliste par une trace ``relationnelle'' pour le débogage de bases de données déductives",
   editor = "O. Ridoux",
   pages = "151-165",
   booktitle = "Journées francophones de Programmation Logique et programmation par Contraintes",
   year = "1998",
   organization = "JFPLC'98",
   publisher = "Hermes",
   address = "Nantes",
   month = "mai",
   Url = {ftp://ftp.irisa.fr/local/lande/sm-md-jfplc98.ps.gz},
   Keywords = {bases de données déductives, débogage, trace, sémantique opérationnelle, multi-SLD-AL, méta-interprète, ensembles de substitutions, instrumentation},
   Abstract = {Le développement des bases de données déductives nécessite des outils, en particulier pour le débogage. Les bases de données déductives gèrent des quantités importantes de données et, en général, de manière ensembliste. Les systèmes d'explication existants pour les bases de données déductives ne prennent pas en compte ces contraintes. Nous proposons une technique de traçage qui consiste à intégrer une trace ``relationnelle'' avec un méta-interprète instrumenté utilisant des ensembles de substitutions. La trace relationnelle donne, de manière efficace, de l'information précise sur l'extraction de données de la base relationnelle. Le méta-interprète ensembliste gère des ensembles de substitutions et donne des explications sur la déduction. Les aspects coûteux de la méta-interprétation sont réduits par l'utilisation de la trace qui évite beaucoup de calculs. La flexibilité de la méta-interprétation est conservée. Elle permet de produire facilement des traces de profils différents.} 
   }
   

1. M. Ducassé. Coca: A Debugger for C Based on Fine Grained Control Flow and Data Events. Technical report IRISA PI 1202 or INRIA RR-3489, INRIA, septembre 1998. [WWW] Keyword(s): Software engineering, Programming environment, Automated debugging, Trace query mechanism, Debugging language, Program behavior understanding, C Debugging tool. Abstract:

   We present Coca, an automated debugger for C, where the breakpoint mechanism is based on events related to language constructs. Events have semantics whereas source lines used by most debuggers do not have any. A trace is a sequence of events. It can be seen as an ordered relation in a database. Users can specify precisely which events they want to see by specifying values for event attributes. At each event, visible variables can be queried. The trace query language is Prolog with a handful of primitives. The trace query mechanism searches through the execution traces using both control flow and data whereas debuggers usually search according to either control flow or data. As opposed to fully ``relational'' debuggers which use plain database querying mechanisms, Coca trace querying mechanism does not require any storage. The analysis is done on the fly, synchronously with the traced execution. Coca is therefore more powerful than ``source line'' debuggers and more efficient than relational debuggers.

   
   

   @TechReport{ducasse98,
   Author = {M. Ducassé},
   url = {http://www.irisa.fr/lande/ducasse/coca-irisa-98.ps.gz},
   Title = {Coca: A Debugger for {C} Based on Fine Grained Control Flow and Data Events},
   Year = {1998},
   Institution = {INRIA},
   Number = {IRISA PI 1202 or INRIA RR-3489},
   Month = {septembre},
   keywords = {Software engineering, Programming environment, Automated debugging, Trace query mechanism, Debugging language, Program behavior understanding, C Debugging tool},
   abstract = {We present Coca, an automated debugger for C, where the breakpoint mechanism is based on events related to language constructs. Events have semantics whereas source lines used by most debuggers do not have any. A trace is a sequence of events. It can be seen as an ordered relation in a database. Users can specify precisely which events they want to see by specifying values for event attributes. At each event, visible variables can be queried. The trace query language is Prolog with a handful of primitives. The trace query mechanism searches through the execution traces using both control flow and data whereas debuggers usually search according to either control flow or data. As opposed to fully ``relational'' debuggers which use plain database querying mechanisms, Coca trace querying mechanism does not require any storage. The analysis is done on the fly, synchronously with the traced execution. Coca is therefore more powerful than ``source line'' debuggers and more efficient than relational debuggers.} 
   }
   

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Les documents contenus dans ces répertoires sont rendus disponibles par les auteurs qui y ont contribué en vue d'assurer la diffusion à temps de travaux savants et techniques sur une base non-commerciale. Les droits de copie et autres droits sont gardés par les auteurs et par les détenteurs du copyright, en dépit du fait qu'ils présentent ici leurs travaux sous forme électronique. Les personnes copiant ces informations doivent adhérer aux termes et contraintes couverts par le copyright de chaque auteur. Ces travaux ne peuvent pas être rendus disponibles ailleurs sans la permission explicite du détenteur du copyright.

This document was translated from BibT_EX by bibtex2html