Résumés des démonstrations et posters
|
|
Démo - Recherche adaptative et contraintes musicales
|
|
Auteur(s) : Charlotte Truchet ( IRCAM)
|
Résumé :
Nous présentons deux prototypes de solvers de contraintes dans OpenMusic.
OpenMusic est un langage visuel pour la composition assistée par ordinateur
basé sur Common Lisp/CLOS. Nous avons intégré à OpenMusic un solver par
backtracking en Lisp, appelé Screamer (Screamer comporte aussi un solver par
propagation qui sera ajouté ultérieurement). Parallèlement, nous présentons une
implémentation d'un algorithme de recherche locale, appelé recherche
adaptative, dans le domaine musical. La recherche adaptative reprend le
principe de résolution par optimisation d'une fonction de coût, mais en
affinant la notion de coût de manière à tenir compte du poids de chaque
variable. Les deux solvers se complètent bien pour résoudre des problèmes
musicaux.
|
Mots clés :
programmation par contraintes, CSP, recherche locale, recherche adaptative, contraintes musicales, composition assistée par ordinateur, séries tous intervalles, Screamer
|
|
|
Démo - Boosting et programmation logique inductive
|
|
Auteur(s) : B. Gil F. Noël M. Sordi N. Soules S. Villefaunes ( IRIT - UMR CNRS 5505 - Université Paul Sabatier - Toulouse)
|
Résumé :
La programmation logique inductive est un des multiples aspects de
l'apprentissage. La méthode de boosting, initialement développée pour des
classificateurs, consise à faire tourner en boucle une machine apprenante pour
générer un nombre fini n d'hypothèses intermédiaires hi, i dans [1,n]. Entre
chaque tour de boucle, les poids des exemples sont modifiés de manière ad-hoc.
Le résultat final h est alors une combinaison linéaire des fonctions
intermédiaires hi. On montre formellement que l'hypothèse finale h est plus
performante que les hypothèses intermédiaires hi. D'où l'idée d'adapter la
méthode à la programmation logique inductive et de valider le processus sur
des bases de données de taille raisonnable. La démonstration que nous proposons
consiste donc en l'exécution d'un prototype développé à l'IRIT Toulouse en 2
mois à partir d'un interprète Progol. Initialement développé à l'Université
d'York, Progol est un des outils les plus répandus en apprentissage inductif.
L'exécution en boucle de l'interprète, en faisant varier entre chaque boucle
l'ensemble d'exemples, génère donc des hypothèses distinctes qui sont en fait
des programmes logiques. A la fin de la procédure, un vote majoritaire est
implanté pour choisir la réponse à une requête Q posée au système.
|
Mots clés :
apprentissage, logique inductive, boosting
|
|
|
Démo - Localisation des erreurs par slicing dans les programmes logiques avec contraintes
|
|
Auteur(s) : Ulrich Neumerkel ( Université Technique de Vienne)
|
Résumé :
Nous présentons des outils pour expliquer les phénomènes inattendus des
programmes logiques avec contraintes (PLC). Lesdits outils s'appuient sur
des lectures sélectives adaptées aux besoins éducatifs. Les techniques
développées localisent des erreurs en déterminant un fragment exécutable du
programme, appelé slice ou tranche. Afin d'enlever l'erreur dans le programme
original, il est indispensable de modifier le fragment proposé par le système.
Par contre, si on ne modifie que des parties hors du fragment, l'erreur
persistera. Nos outils ont été intégrés dans un environnement de
programmation spécialisé pour l'enseignement de la PLC, facilitant les
lectures sélectives pour l'échec inattendu, les solutions inattendues et
la non terminaison.
|
|
|
Démo - TCLP: Programmes logiques avec contraintes typés
|
|
Auteur(s) : Emmanuel Coquery ( INRIA Rocquencourt)
|
Résumé :
TCLP est un programme de typage pour la programmation logique avec contraintes,
utilisant le sous-typage et le polymorphisme paramétrique,
basé sur la bibliothèque de sous-typage Wallace de F.Pottier.
Son objectif est la détection statique d'erreurs de programmation.
Il introduit une discipline de typage simple pour les programmes logiques avec
contraintes qui autorise, via le sous-typage, les coercions usuelles entre
les domaines de contraintes et le typage de la méta-programmation.
TCLP lit des sources Prolog (ISO ou Sicstus), et effectue une vérification
de types à l'aide de déclarations de types pouvant être incluses dans
les sources à vérifier. Il est également possible d'inférer des types
pour des prédicats non déclarés.
|
Mots clés :
sous-typage, polymorphisme paramétrique, programmation logique, programmation par contraintes, vérification de types, inférence de types
|
|
|
Démo - HyperPro - Un environnement intégré de documentation pour la PLC
|
|
Auteur(s) : AbdelAli Ed-Dbali ( LIFO - Université d'Orléans)
|
Résumé :
Le but de cette démonstration est de présenter certaines fonctionnalités du système HYPERPRO. HYPERPRO est un environnement de développement integré pour la PLC (programmation en logique et par contraintes) qui offre deux aspects du développement d'un programme : le codage en PLC et la documentation. Un document HYPERPRO est donc une combinaison de code et de sa documentation. La partie édition d'HYPERPRO est basé sur le système Thot. HYPERPRO est un éditeur WYSIWYG qui offre des facilités de navigation hypertexte, de manipulation de versions d'un même programme, d'extraction de vues projections selon des critères spécifiques. Il offre également l'exportation de document vers plusieurs formats courants (ps, html, latex, ...) ainsi que la gestion des indexes. HYPERPRO a été conçu pour la PLC mais il peut aussi bien être adapté à d'autres paradigmes de programmation.
|
Mots clés :
PLC, programmation littéraire, gestion de versions, édition structurée, hypertexte, documentation, spécification
|
|
|
Poster - GUPU - un environnement pour l'enseignement de Prolog et de la PLC
|
|
Auteur(s) : Ulrich Neumerkel ( Université Technique de Vienne)
|
Résumé :
GUPU est un environnement de programmation spécialisé pour l'enseignement de
Prolog et de la programmation logique avec contraintes. Notre approche repose
sur une technique de lecture sélective textuelle à plusieurs niveaux. Par
rapport aux approche courantes, les aspects déclaratifs, comme également
quelques propriétés opérationnelles essentielles - en particulier, la
terminaison ainsi que la non terminaison - son expliqués tout en évitant les
notions d'arbres de preuve et les traces. L'environnement GUPU a les
caractéristiques suivantes:
- langage Prolog pur et extensions de la PLC, CLP(FD) de SICStus.
- intégration de toute activité de programmation dans une seule commande
(sauvegarde, validation syntaxique, compilation, chargement, test d'assertions,
pré-notation) permettant un retour immédiat par rapport à l'état du système.
- pratique d'écrire les test (assertions) puis coder - récement vulgarisée par
le mouvement extreme programming - mettant l'accent sur la spécification du
problème.
- pré-notation automatisée et instantanée.
- validation de la syntaxe (indentation, orthographe etc.) pour renforcer des
standard de codage et remédier aux difficultés de la syntaxe édimbourgeoise
fragile.
- inférence de condtions de terminaisons (cTI).
- vérification de la non-terminaison (NTI).
- explication des phénomènes inattendus pour supporter des lectures
sélectives.
- affichage des graphismes sans effet de bords et animation du processus
d'instantiation.
- messagerie intégrée dans le texte du programme.
- dialogues trilingues (allemand/français/anglais).
|
|
|
Poster - Fractions : outils de vérification de propriétés par des techniques de
|
|
Auteur(s) : Fabrice Parrennes ( Université Paris 6, LIP6 -- SURLOG S.A.)
|
Résumé :
Ce poster présentera une technique de vérification de propriétés de programmes
fondée sur la résolution de contraintes.
Cette technique est utilisée pour des programmes réactifs de type contrôle
commande. Ces programmes sont traduits auparavant, grâce à l'outil AGFLr (1),
en une famille de programmes très simples, ne comportant que des affectations
gardées. Cette classe de programmes peut être traduite vers un langage
constitué d'un noyau impératif sans récursion. Les propriétés étudiées sont
décrites dans le même langage et portent sur l'aspect
fonctionnel/dysfonctionnel du programme étudié.
L'outil Fraction implémente cette analyse. Il est basé sur une interprétation
des propriétés d'un programme par des contraintes et une bibliothèque de
simplification permet d'obtenir une forme normalisée des contraintes utilisées.
On utilise alors des outils externes de vérification de contraintes pour
valider plus finement les propriétés recherchées.
L'utilisation de techniques liées aux contraintes pour la vérification des
propriétés n'est pas véritablement nouvelle, que ce soit dans l'univers de la
vérification de modèle ou dans des techniques de recherche de jeux de test
logiciel. L'originalité de l'approche consiste à combiner une analyse statique
de programme et une représentation sous forme de contraintes des propriétés.
Les propriétés recherchées et les programmes analysés sont exprimés eux-mêmes
dans un langage unique de contraintes.
La validation de l'approche utilise des mécanismes semblables à ceux utilisés
en interprétation abstraite, une correspondance entre contraintes et propriétés
est établie et un algorithme de simplification (basée sur une sémantique à
réduction des domaines) permet d'obtenir une forme normalisée où à chaque
contrainte est associée un unique ensemble de valeurs. Dans ce cadre, la
validation de l'abstraction d'une propriété se ramène alors à un problème de
satisfaction de contraintes et les techniques habituelles d'interprétation
abstraite permettent de conclure sur la validité de la propriété.
--
(1) AGFLr (Analyse par Graphe Fonctionnel du Logiciel) est un outil développé par SURLOG S.A.
|
Mots clés :
vérification de propriétés, interprétation abstraite, résolution de
|
|