Boolean Expression
h3>5.1 State-Based Specifications
State-based specifications describe software systems in terms of states and effects of operations on states. Tais especificações são suportadas por várias linguagens de especificação, que agrupamos em dois conjuntos: linguagens de especificação clássicas, como Z , B , e VDM , e linguagens de afirmação, como Eiffel , JML (Java Modeling Language) , e tabelas de Peters e Parnaso . Enquanto as linguagens clássicas de especificação definem estados e transições independentemente da implementação, as linguagens de asserção especificam estados e transições como declarações ou anotações do programa fonte.
Especificações baseadas em estados são usadas como oráculos de teste verificando a conformidade das execuções de teste com as especificações. O principal problema na geração de oráculos de teste a partir de especificações baseadas em estados vem dos diferentes níveis de abstração entre as especificações e as operações monitoradas durante a execução do teste; assim, as especificações das operações serão traduzidas de uma forma verificável. Os idiomas das especificações são geralmente expressivos o suficiente para representar várias estruturas de dados e propriedades baseadas no estado, mas sua expressividade complica a tradução para a forma executável. Muitas vezes a tradução faz algumas suposições simplificadoras, como a limitação de conjuntos infinitos, por exemplo, o conjunto infinito de números naturais, e o manuseio de elementos não executáveis apenas parcialmente e às vezes exigindo alguma intervenção humana.
Aqui, discutimos as principais abordagens para traduzir especificações baseadas no estado para uma forma executável. A tradução das especificações Z, B e VDM apresenta os mesmos problemas relacionados a infinitas estruturas de dados, expressões parcialmente definidas e estruturas orientadas a objetos. A tradução de Eiffel, JML e outras linguagens de asserção em forma verificável apresenta problemas semelhantes, mas com um nível de abstração diferente. A seguir, apresentamos as principais abordagens para traduzir as especificações baseadas no estado em forma verificável referentes ao Z; as abordagens para outras línguas são semelhantes. Em seguida, discutimos os problemas de compilação de asserções em verificações executáveis referentes a Eiffel, JML e tabelas de Peters e Parnaso.
O esquema de compilação predicada proposto por Mikk compila as especificações Z em código C. Para cada esquema Z, que é a unidade básica em Z, a abordagem gera uma função C que avalia o esquema prediz usando o estado do programa passado para a função como um parâmetro. O código gerado avalia os predicados do esquema com uma estratégia de “força bruta”: Dado um estado, o código substitui essencialmente expressões com seus valores, avalia fórmulas de cálculo proposicionais usando tabelas de verdade e avalia quantificações e construções de conjuntos, iterando através das estruturas de dados. Para reduzir a complexidade das funções C geradas, a abordagem propõe uma etapa de otimização para garantir que o código C gerado termine sempre. Para otimizar o código, a técnica define um subconjunto “executável” da linguagem Z. O subconjunto consiste em previsões finitas, tais como fórmulas de cálculo proposicional, quantificações sobre conjuntos finitos e construções de conjuntos baseados em iteração finita. A técnica estende o conjunto de predicados executáveis com um conjunto de regras para transformar predicados especiais não executáveis que satisfazem certas condições em executáveis sem alterar a sua semântica. Por exemplo, as duas regras a seguir eliminam os quantificadores:
onde M é um conjunto, a variável x representa um elemento em M, e P é um predicado. O operador – também conhecido como “Z notation spot”, significa “aquele” quando usado com o quantificador ∃ e “aquele”, quando usado com o quantificador ∀. Por exemplo, ∃ x : M – P significa que existe pelo menos um valor x em M tal que o predicado P é verdadeiro. A condição NotOccur(x, P) indica que x não é uma variável livre no predicado P. Embora o conjunto M possa ser infinito, o compilador ainda pode compilar especificações usando quantificadores sobre M desde que os quantificadores possam ser eliminados pela aplicação das regras acima. Para funções definidas pelo usuário que podem ser introduzidas por definições axiomáticas ou genéricas, o compilador requer que o usuário forneça o código correspondente. Mikk propõe também uma solução para o problema das especificações parcialmente definidas. Ele usa o VDM-SL como uma forma intermediária e o compilador VDM-SL desenvolvido por Schmidt e Hörcher para traduzir as especificações Z para o código C. Quando se trata de expressões parcialmente definidas, ou seja, funções ou relações que podem avaliar indefinidas (denotadas como ⊥) quando avaliadas fora de seu domínio de definição, a abordagem gera manipuladores de exceção.
Extensões orientadas a objeto de Z, como Objeto-Z, exacerbam os problemas. McDonald et al. traduzem as especificações Ojbect-Z das classes container em código C++ em três etapas: otimização, mapeamento estrutural e tradução predicada . No estágio de otimização, eles reorganizam a especificação para simplificar a tradução subsequente através de várias etapas, incluindo a substituição de variáveis constantes por seus valores e a remoção de variáveis secundárias e enriquecimento de esquemas. No estágio de mapeamento estrutural, eles mapeiam estruturas na especificação Objeto-Z para seus respectivos elementos de código: Constantes de especificação e variáveis a variáveis com inicializações adequadas, e tipos de variáveis a tipos C++ primitivos ou classes correspondentes na biblioteca de ferramentas Z utilizada pela técnica. Por exemplo, eles mapeiam os tipos inteiros e booleanos para int, e o tipo de conjunto inteiro para z_set<int >. Eles mapeiam o esquema de inicialização para um construtor, e esquemas de operação para funções de membro, criam uma função de membro especial, inv(), para verificar a invariância da classe, e geram uma classe de exceção para cada esquema de exceção.
Na tradução predicate DeepL, a técnica foca em como gerar código para verificar o estado do programa, em vez de avaliar predicados. Por exemplo, a tradução impede que a função inv() chame qualquer outra função de membro, para evitar a repetição infinita. Em um construtor, a classe invariant é verificada na sua saída.
Richardson et al. focam em sistemas críticos de tempo, lidam com uma combinação de Z e lógica de intervalo temporal, e propõem uma tradução de especificações em oráculos de teste por meio de interpretação simbólica. A interpretação simbólica atribui os nomes simbólicos nas especificações às entradas de estímulos e às variáveis de estado inicial, através da referência aos dados e mapeamentos de controle. Em seguida, a interpretação simbólica interpreta cada caminho de controle nas especificações, ou seja, cria uma asserção expressando a condição nos dados da especificação com base no estado simbólico em cada ponto de controle da especificação. Um ponto de controle de especificação é um elemento relevante, tal como um evento parametrizado, uma transição e uma operação. Após a interpretação simbólica da especificação Z, a informação do oráculo é representada como uma lista de esquemas Z relevantes e suas respectivas asserções, que são verificadas se o esquema for invocado. A execução de um caso de teste refere-se a uma entrada de teste concreta a partir da qual variáveis e eventos concretos são ligados às suas contrapartes na classe de teste (cada classe de teste é uma partição da entrada de teste). A execução do caso de teste produz um perfil de execução, e os eventos e valores concretos das variáveis contidas no perfil de execução são mapeados para o nível do oráculo para verificar sua consistência com as informações do oráculo.
Línguas de teste fundem especificações com o código fonte, simplificando assim, mas não eliminando o problema de tradução. As asserções são suportadas por diferentes idiomas e metodologias. Design por contrato é um paradigma de design de software que postula o design conjunto de código e asserções. Design por contrato foi proposto por Meyer e é totalmente suportado pela linguagem de programação Eiffel . Diferentemente das linguagens de especificação geral, como Z, as especificações em Eiffel, chamadas contratos, são fundidas no código fonte e definem obrigações e benefícios dos componentes de software que se comunicam através de interfaces bem projetadas. Nas linguagens de suporte aos contratos, as obrigações e benefícios dos clientes são expressos como pré e pós-condições dos prestadores de serviços. O código-fonte é enriquecido com invariantes que representam propriedades estatais que devem ser mantidas durante qualquer interação.
Contratos foram estendidos para muitas linguagens. iContract foi a primeira ferramenta a suportar contratos em Java . No iContract, os contratos são escritos como comentários de código com tags especiais. Os contratos suportados pelo iContract são expressões booleanas compatíveis com a sintaxe Java, excepto para algumas extensões sintácticas que incluem a quantificação universal (∀), a quantificação existencial (∃), e a implicação (→). Estas extensões foram concebidas para simplificar a sua tradução em código Java. Por exemplo, a tradução para código Java, the syntax of ∀ is forall < Class >< var > in < Enum >< Exp_var >, where < Class > is the type of the variable < var >, which represents an element of < Enum >. A reasonable translation of the ∀ expression is to use a Java loop to iterate over the enumeration < Enum > and evaluate the boolean expression < Exp_var > in each iteration. The existential quantification is translated similarly. An implication expression C implies I can be simply translated into an if statement: “se C então verificar I.”
Beside a tradução simples de expressões booleanas, iContract aborda questões relacionadas ao ciclo de vida do objeto, o escopo das variáveis, e a herança, a maioria das quais são específicas da programação orientada ao objeto. As regras mais importantes relacionadas ao ciclo de vida do objeto são as seguintes:
Na construção de um objeto, as pré-condições devem ser verificadas no início da construção, enquanto que as invariantes e as pós-condições são verificadas apenas se a construção terminar normalmente (sem exceções).
Para invocações normais do método em objetos, as pré-condições e pós-condições são verificadas na entrada e saída dos métodos invocados, e as invariantes não são verificadas para métodos privados.
Na destruição do objeto, nenhuma verificação é necessária. Assim, nenhum código de verificação é inserido nos métodos finalize().
Os predicados usados nas condições pós-condições frequentemente referem-se tanto ao valor de retorno do método como ao valor “antigo” (ou “valor de entrada”) de algumas variáveis. iContract sintetiza uma pseudo-variável, chamada return, para representar o valor de retorno, armazena os valores das variáveis na entrada, e os torna acessíveis como os nomes das variáveis com as expressões postfix @pre. Como resultado, pode haver potenciais recorrências infinitas na verificação de invariantes. Para resolver este problema, iContract mantém o controle da profundidade de recursividade para cada objeto dentro de cada thread e verifica apenas invariantes com profundidade 0. Os mecanismos de extensão de tipo em Java têm várias implicações sobre como os contratos dos tipos devem ser tratados. iContract propaga contratos seguindo estas regras:
Invariantes são conjuncionadas, ou seja, a invariante de um subtipo é a conjunção das invariantes de todos os seus supertipos.
Pós-condições são conjuntadas, ou seja, a condição de um subtipo é a conjunção das condições de todos os seus supertipos.
Precondições são disjuntas, ou seja, a condição de um subtipo é a disjunção das condições de todos os seus supertipos.
JML é uma linguagem de especificação comportamental popular que suporta Design by Contract em Java . Os contratos de JML estão na forma de comentários especiais em Java. JML expressa pré-condições, pós-condições, e invariantes como expressões booleanas precedidas pelas palavras-chave requer, assegura, e invariantes, respectivamente, e usa método embutido \ old(x) para representar o valor de x antes de uma operação. Similar à notação ▵ em Z, JML fornece a palavra-chave modificada para indicar as variáveis que são alteradas no corpo de um método. Além disso, JML lida com várias características orientadas a objetos, tais como visibilidade e herança.
JML é a base de muitas abordagens para testar a geração de oráculos. Bhorkar propôs uma técnica para traduzir contratos JML em asserções Java . Apesar de suportar apenas condições prévias, esta técnica aborda questões relacionadas a variáveis apenas de especificação, refinamento, herança de especificação e privacidade. Semelhante ao iContract, a técnica lida com a herança de contratos através da conjunção e disjunção dos contratos de acordo com seus tipos. A técnica também usa uma tabela de hash (por thread) para evitar repetições na verificação em tempo de execução. Expressões usando quantificadores são consideradas como não executáveis pela técnica, e nenhum código Java é gerado para tais expressões.
Korat propôs uma técnica para gerar tanto casos de teste como oráculos a partir de especificações JML . A técnica de Korat gera casos de teste a partir de pré-condições e invariantes e oráculos a partir de pós-condições e invariantes. Araujo et al. ampliaram o JML adicionando contratos simultâneos e propuseram um suporte em tempo de execução para permitir a verificação de afirmações que especificam propriedades simultâneas .
Peters e Parnaso introduziram uma abordagem para gerar oráculos de teste a partir de documentação formal . A documentação é dada em uma forma tabular que consiste em relações que especificam as interfaces de procedimentos e é traduzida em oráculos em código C e C++. O elemento central da documentação formal consiste em expressões predicadas escritas em uma variante da lógica predicada com construções especiais para lidar com funções parciais. Similar a outras técnicas de oráculos baseadas em especificações, esta técnica trata quantificadores restringindo-os a conjuntos finitos.
Para permitir iterações sobre conjuntos de elementos com quantificadores, Peters e Parnaso introduzem predicados definidos indutivamente. Para um conjunto S (a ser usado em quantificações), um predicado P definido indutivamente é definido com três elementos I, G e Q. O conjunto inicial I contém um número finito de elementos, G é uma função, chamada “função geradora”, que gera os elementos do conjunto, e Q é um predicado que caracteriza as propriedades do conjunto. O conjunto S é definido como o menos conjunto construído nos passos indutivos abaixo:
S0 = I
Sn + 1 = Sn ∪ {G(x)|x ∈ Sn ∧ Q(x)}
I, G e Q devem ser definidos para satisfazer uma condição especial que garanta que o conjunto construído S é finito .
Peters e Parnaso propõem uma abordagem para traduzir as documentações tabulares em código C . Como a forma das expressões usadas nas documentações é bem definida, a tradução é feita sistematicamente.
Outras especificações baseadas no estado também são usadas para derivar oráculos de teste. Os modelos UML são geralmente informais; no entanto, Bouquet et al. definiram um subconjunto de UML 2.1, denominado UML-MBT, que é suficientemente preciso para gerar automaticamente casos de teste. UML-MBT inclui diagramas de classes, máquinas de estado e um subconjunto de OCL 2.0. Bouquet et al. usam especificações escritas em VDM-SL para gerar oráculos de teste.