Paquet : cafeobj (1.6.0-2)

langage de spécification et programmation algébrique de nouvelle génération

CafeOBJ est un langage de spécification formelle évolué qui hérite de beaucoup des fonctionnalités du langage de spécification algébrique OBJ (OBJ3, plus précisément), dont une syntaxe mini-fix flexible, un système de typage puissant et clair avec des tris ordonnés, des modules et vues paramétriques pour instancier les paramètres, des expressions de modules, etc.

CafeOBJ est un langage servant à écrire des spécifications formelles (c'est-à-dire mathématiques) de modèles pour une grande variété de logiciels et de systèmes et vérifier leurs propriétés. CafeOBJ implémente la logique équationnelle par réécriture et peut servir de système de preuve de théorème interactif et puissant. Les rédacteurs de spécifications peuvent écrire des preuves en CafeOBJ et les vérifier en les exécutant.

CafeOBJ dispose de sémantiques logiques rigoureuses de pointe basées sur les institutions. Le cube CafeOBJ montre la structure des diverses logiques sous-jacentes de la combinaison de plusieurs paradigmes implémentés par le langage. Les preuves en CafeOBJ sont aussi basé sur des sémantiques rigoureuses basées sur les institutions et peuvent être construites grâce à un ensemble complet de règles de preuve.

Cette page est uniquement disponible dans les langues suivantes (Comment configurer la langue par défaut du document) :