CafeOBJ e ARCCafeOBJ e ARCCafeOBJ e ARCCafeOBJ e ARC

Carlos Cunha

ceac@cin.ufpe.br

TópicosTópicos

UTP e ARC Trabalho

Modulo Alphabet Modulo Predicado

Modulo UTP Operadores e Funções Leis

Problemas Trabalhos Futuros

TrabalhoTrabalho

CafeOBJ Compilador LISP

Especificação das leis do ARC Modulos criados para ajuda em provas Modulos:

Predicate Alphabet List*

UTP e ARCUTP e ARC

Nuka, G., Woodcock, J. Mechanising the Alphabetized Relational Calculus. IV Worshop de Métodos Formais, WMF’03, pages 152-165, Campina Grande, Brasil.

Interface para Paradigmas de Programação

Modulo AlphabetModulo Alphabet

Ilustrativo Mesmo assim:

Ponto de partida Definição de algumas funções básicas

Modulo PredicateModulo Predicate

Definição dos operadores e funções Utilizado:

Definição dos axiomas

Modulo UTP Axiomas gerais Provador dos teoremas

OperadoresOperadores

União Intersecção Implicação Equivalência

FunçõesFunções

Alpha Bound Binding Set Extending Set Restrict Set

LeisLeis

Algumas são provadas implicitamente pelas propriedades dos operadores

Outras exploradas através do cálculo de Tarski

Contudo algumas não foram especificadas

LeisLeis

Lei 23 : betha( n ∀ • m ∀ • p) = betha( m ∀ • n ∀ • p)

Lei 24 : betha( n ∃ • m ∃ • p) = betha( m ∃ • n ∃ • p)

ProblemasProblemas

Falta de Bibliografia Operadores existencial e universalidade Sistema

Inconsistente? Difícil utilização Bugs?

Trabalhos FuturosTrabalhos Futuros

OhCircus: Baseada em UTP Suporte a semântica

Formula