Abstract FR:

La necessite de maitriser la complexite des logiciels conduit a s'interesser au processus de leur construction: la specification decrit ce que doit faire le logiciel, et le programme, qui explicite comment il doit le faire, doit satisfaire cette specification. Le travail que nous presentons est centre sur le langage de developpement deva, qui est un lambda-calcul type, avec types dependants. Il permet, dans le cadre de l'isomorphisme de curry-howard, de representer les preuves en logique constructive. Dans ce contexte, developper un programme a partir d'une specification consiste a prouver que le programme obtenu satisfait la specification, et une methode de developpement est la theorie qui permet de faire cette preuve. Les developpements totalement formalises sont extremement lourds, et nous proposons deux solutions pour alleger le travail de developpement: les definitions implicites et les modules. Les definitions implicites permettent de designer les parametres pour lesquels l'argument correspondant est synthetise automatiquement par l'outil de validation, a partir des informations qu'il peut deduire des autres arguments. Les modules sont des objets persistants. Ils enregistrent methodes et developpement et une fois valides, peuvent etre references dans de nouveaux developpements. La definition que nous en donnons permet de resoudre le probleme du partage des informations entre modules