A sequência de funcionamento do plug-in SMT para Rodin pode ser resumida em três etapas, relacionadas abaixo. Apresentam-se maiores detalhes sobre cada etapa nas Subseções 4.3.1, 4.3.2 e 4.3.3. Uma visão esquemática da execução do plug-in é ilustrada na Figura 15.
1. Tradução: Um sequente que representa determinada obrigação de prova é enviado ao plug-in para ser traduzido da notação Event-B ao formato SMT-LIB;
2. Verificação: Um solucionador SMT é invocado para verificação da fórmula SMT; 3. Resposta: A resposta do solucionador (sat, unsat ou unknown) é enviada de volta
Figura 15: Visão esquemática do funcionamento do plug-in SMT para Rodin
Fonte: Déharbe et al. (2014a)
4.3.1
Tradução
A maior parte da notação encontrada nos sequentes Event-B possui correspondência em SMT-LIB. Constantes e operadores booleanos, operadores relacionais e a maioria dos símbolos aritméticos podem ser submetidos à tradução sintática direta. Os operadores de divisão e exponenciação são traduzidos como símbolos não interpretados. Isto se deve a divergências de tratamento desses operadores por diferentes provadores (ALMEIDA, 2013).
Por exemplo, o operador de divisão é representado por "/" em veriT e por div em Z3 (MOURA; BJORNER, 2008).
Para exemplificar a tradução de uma obrigação de prova para o formato SMT-LIB, seja o seguinte sequente 0 < n ⊢ n − 1 ∈ N e ambiente de tipo n: Z. O script SMT ilustrado a seguir, na Figura 16, é criado como resultado da tradução. É importante notar que o processo de transformação envolve a negação da conclusão do sequente. Isto acontece
porque o solucionador SMT deverá verificar a validade da obrigação de prova, isto é, a insatisfatibilidade da fórmula negada.
( set-logic AUFLIA) ( declare-fun n ( ) I n t ) ( assert (< 0 n ) )
( assert ( not (<= 0 (− n 1 ) ) ) ) ( check-sat )
Figura 16: Tradução de um sequente simples para o formato SMT-LIB
A representação de símbolos de teoria dos conjuntos é o principal desafio no processo de transformação, já que segundo Déharbe (2013), "atualmente nenhum solucionador SMT provê suporte direto à teoria dos conjuntos". Neste sentido, o plug-in conta com duas abordagens de tradução, descritas a seguir: abordagem com expressões lambda e abordagem com ppTrans.
4.3.1.1 Abordagem com expressões lambda
Esta abordagem de tradução é baseada numa versão estendida de SMT-LIB, su- portada pelo solucionador veriT. Tal extensão consiste na implementação de expressões lambda, definições macro e tipos polimórficos. A partir destas extensões é possível obter uma representação de conjuntos simples (não há suporte a conjuntos de conjuntos), em que cada conjunto é representado por sua função indicadora e os operadores são constituídos por conectivos booleanos.
Assim, um conjunto é traduzido para uma função booleana que recebe como argu- mento um valor de tipo correspondente ao conjunto a ser representado. Exemplos de operações incluem valor falso para conjunto vazio, disjunção para união, implicação para inclusão e aplicação de predicado para pertinência. Exemplifica-se a tradução de alguns conjuntos a seguir (DÉHARBE et al., 2014a): o conjunto unitário {1} é identificado como
(λx : Z | x = 1); o conjunto vazio com a expressão lambda polimórfica (λx : X | F ALSE), onde X é uma variável de tipo; e a união de conjuntos como a função polimórfica de ordem superior (λ(S1: X → BOOL) 7→ (S2: X → BOOL) | (λx : X | S1(x) ∨ S2(x))).
O sequente A: P(Z) ⊢ A ∪ {a} = A é traduzido para o script SMT ilustrado na Figura 17.
( declare-fun A ( I n t ) Bool ) ( declare-fun a ( ) I n t ) ( define-fun ( par (X)
( union ( ( S1 (X Bool ) ) ( S2 (X Bool ) ) ) (X Bool ) ( lambda ( ( x X) ) ( or ( S1 x ) ( S2 x ) ) ) ) ) )
( define-fun enum ( ( x I n t ) ) Bool (= x a ) ) ( assert ( not (= ( union A enum ) A) ) ) ( check-sat )
Figura 17: Script SMT-LIB exemplificando tradução com expressões lambda
Fonte: Déharbe et al. (2014a)
O tradutor insere definições de funções, sendo a função enum a representação do con- junto {a} e union a definição macro relativa à união de conjuntos. Uma lista destas definições, suportadas pelo plug-in, pode ser encontrada em Almeida (2013). Descrevem- se detalhes do mecanismo de extensão a SMT-LIB para suporte a expressões lambda e polimorfismo em Bonichon, Déharbe e Tavares (2014). Enfatiza-se ainda que veriT pode gerar, em parte dos casos, uma fórmula de primeira ordem em SMT-LIB padrão para que seja possível a verificação por outros solucionadores SMT.
Além da limitação referente à impossibilidade de representação de conjuntos de con- juntos, a abordagem de tradução com expressões lambda torna a utilização do plug-in atrelada a veriT, mesmo que este seja usado apenas como pré-processador para geração de fórmulas SMT compatíveis com outros solucionadores. Por tais motivos a utilização desse mecanismo tem sido desencorajado em favor da tradução com ppTrans (SMT Solvers Plug-in, 2014).
4.3.1.2 Abordagem com ppTrans
Esta abordagem de tradução consiste na transformação de sequentes Event-B, pre- viamente simplificados pelo tradutor ppTrans (disponível na Plataforma Rodin), para o formato SMT-LIB. Konrad e Voisin (2012) descrevem o mecanismo de simplificação, que consiste na reescrita de obrigações de prova produzidas por Rodin a um subconjunto da notação Event-B. Algumas regras de reescrita são ilustradas na Tabela 4. Uma listagem completa delas pode ser obtida no trabalho supracitado. Os autores relacionam as seguin- tes características de tradução: eliminação da maior parte dos símbolos relativos à teoria
dos conjuntos; separação das construções aritméticas daquelas relacionadas a conjuntos; e simplificação de predicados.
Tabela 4: Algumas regras de reescrita implementadas por ppTrans Notação Event-B Versão simplificada
x 6= y ¬(x = y) x /∈ s ¬(x ∈ s) s ⊆ t s ∈ P(t) s* t ¬(s ∈ P(t)) s ⊂ t s ∈ P(t) ∧ ¬(t ∈ P(s)) s 6⊂ t ¬(s ∈ P(t)) ∨ t ∈ P(s)) Fonte: Adaptado de Déharbe (2010)
A gramática da linguagem de ppTrans é ilustrada na Tabela 5. Nela, é possível ob- servar que o único símbolo da teoria dos conjuntos é o operador de pertinência ∈.
O processo de tradução para SMT-LIB é iniciado, então, após a simplificação pro- movida por ppTrans. Como explicado por Déharbe et al. (2012, 2014a), há uma série de particularidades inerentes à tradução da operação de pertinência, a saber: produz-se declaração de novos tipos (sorts) para cada novo conjunto (1) ou combinação de conjun- tos (2) e declaração de novas funções para as constantes (3) e para cada um dos tipos presentes no predicado (4).
Por exemplo, seja o sequente A : P(S) ⊢ A ∪ {a} = A; simplificada por ppTrans, a conclusão se torna ∀x.(x ∈ A ∨ x = a) ⇔ x ∈ A. O script SMT-LIB produzido como resultado da tradução é exibido na Figura 18. Os comentários refletem os passos descritos no parágrafo anterior.
Axiomas, tais como o de definição de conjunto unitário, podem ser incluídos no script de modo a auxiliar a interpretação da operação de pertinência, já que sua semântica é uma aproximação daquela em Event-B (DÉHARBE et al., 2012).
4.3.2
Verificação
Após a etapa de tradução, a fórmula SMT resultante (que representa uma obrigação de prova do modelo Event-B a ser verificada) é passada como entrada para um solucionador. Os solucionadores já testados com a ferramenta são veriT, CVC3 (BARRETT; TINELLI, 2007), Z3 e Alt-Ergo, sendo os dois primeiros distribuídos junto com o plug-in, a partir da versão 0.8 (SMT Solvers Plug-in, 2014). Outros solucionadores, ou diferentes versões de
Tabela 5: Gramática de ppTrans P ::= P ⇒ P | P ≡ P | P ∧ . . . ∧ P | P ∨ . . . ∨ P | ¬P | ∀L.P | ∃L.P | A = A | A < A | A ≤ A | M ∈ S | B = B | I = I L ::= I . . . I I ::= N ame A ::= A − A | A ÷ A | A mod A | A exp A | A + . . . + A | A × . . . × A | − A | I | IntegerLiteral B ::= true | I M ::= M 7→ M | I | integer | bool S ::= I
Símbolos não terminais: P (predicados), L (lista de identificadores), I (identificadores), A (expressões aritméticas), B (expressões booleanas), M (expressões de par ordenado), S (expressões de conjuntos)
Fonte: Déharbe et al. (2014a)
um mesmo solucionador, podem ser conectados por meio da interface de preferências da plataforma (opção "SMT").
A execução dos diferentes solucionadores no processo de prova em Rodin está atrelada à criação de configurações: conjuntos de opções modificáveis individualmente para cada provador. É possível definir, por exemplo, listas de parâmetros de entrada e a versão de SMT-LIB a ser utilizada. O usuário tem a opção de criar diferentes configurações para um mesmo solucionador. São disponibilizadas algumas configurações prontas para os solucionadores embutidos no plug-in. Por padrão, utiliza-se a abordagem de tradução ppTrans e SMT-LIB versão 2.0.
A aplicação dos solucionadores SMT é disponibilizada por uma tática (vide Seção 2.6.1.3) no ambiente de prova. Uma tática automática já está configurada nas opções padronizadas do plug-in, mas o usuário pode criar outras táticas a serem utilizadas. Por exemplo, pode ser útil combinar a tática existente para SMT com a execução concomitante de outros provadores disponíveis em Rodin, tais como PP e ML. No ambiente de prova, o usuário poderá selecionar um solucionador SMT específico ou executar sucessivamente todos os que estiverem habilitados, como ilustrado na Figura 19. Informações adicionais sobre uso e configuração do plug-in para o processo de prova podem ser obtidas em SMT Solvers Plug-in (2014). Terminado o processo de verificação pelo solucionador, uma resposta é enviada de volta à plataforma.
( set-logic AUFLIA) ( declare-sort S 0 ) ; (1) ( declare-sort PS 0 ) ; P(S) (2) ( declare-fun A ( ) PS) ; A ∈ P(S) (3) ( declare-fun a ( ) S ) ; a ∈ S (3) ( declare-fun MS0 ( S PS) Bool ) ; ∈ A (4) ( assert (MS0 a A) ) ; a ∈ A
( assert ( not ( forall ( ( x S ) )
(= ( or (MS0 x A) (= x a ) ) (MS0 x A) ) ) ) ) ; conclusão ( check-sat )
Figura 18: Script SMT-LIB exemplificando tradução com ppTrans
Fonte: Adaptado de Déharbe et al. (2014a)
Figura 19: Aplicação de tática SMT em Rodin
4.3.3
Resposta
Como visto no Capítulo 3, solucionadores SMT respondem à questão de satisfatibi- lidade. De acordo com o padrão SMT-LIB (BARRETT; STUMP; TINELLI, 2010b), uma de
três respostas possíveis pode ser reportada ao usuário após a verificação de um script SMT:
1. sat: quando existe um conjunto de atribuições de valores para as constantes e símbolos de funções que tornam verdadeiras todas as asserções declaradas;
2. unsat: quando não há tal conjunto;
3. unknown: quando o solucionador é incapaz de definir se as asserções são ou não satisfatíveis (pode estar relacionado a vários fatores, entre eles falta de memória ou incompletude do solucionador frente à logica na qual a PO é verificada).
Em Rodin, a resposta do solucionador é interpretada como válida (unsat) ou inválida (sat, unknown). Se a resposta for válida, uma nova regra de prova (vide Seção 2.6.1.3) é criada e enviada à plataforma (DÉHARBE et al., 2014a), refletindo na árvore de prova. Do
contrário, o sequente não é verificado e a árvore de prova permanece intacta.
É possível obter informações adicionais sobre cada uma das três respostas passíveis de serem retornadas pelo solucionador. Análise e extração dessas informações são interesses fundamentais deste trabalho, visto que se propõe o aprimoramento do comportamento do plug-in quando uma obrigação de prova não for descartada, isto é, quando o solucionador retornar sat ou unknown. A disponibilidade de informações acerca do resultado retornado está relacionada à capacidade dos solucionadores SMT em gerar provas e contra-modelos ou reportar núcleos insatisfatíveis. Discorre-se sobre estas operações e como se relacionam ao a este trabalho no capítulo a seguir.
4.4
Considerações finais
Neste capítulo, foram explicadas as características do processo de verificação de Satis- fatibilidade Módulo Teoria em Event-B, por meio da Plataforma Rodin. Especificamente, foram apresentados a motivação, os trabalhos relacionados e o funcionamento do plug- in SMT para Rodin, incluindo mecanismos de tradução entre as linguagens Event-B e SMT-LIB, bem como as formas de manipulação dos resultados retornados pelos solucio- nadores. A ideia é não apenas prover uma introdução ao entendimento de como funciona o plug-in, mas também situar o estado deste antes da implementação das contribuições descritas neste trabalho. No Capítulo 5, são descritos a metodologia empregada, detalhes de implementação e resultados obtidos.