Upload
vongoc
View
239
Download
0
Embed Size (px)
Citation preview
1
Assertivas
Arndt von Staa
LES/DI/PUC-Rio
Fevereiro 2018
Fev 2018 2Arndt von Staa © LES/DI/PUC-Rio
Especificação
• Objetivos dessa aula– Estabelecer uma notação rigorosa para assertivas
• deve ser editável com teclado ISO-ASCII
– A notação visa apoiar • a argumentação da corretude de programas
• a implementação de assertivas executáveis
• tornar mais robustos os sistemas em execução
• Justificativa– assertivas tornam mais formais as especificações do código
• são a base para a argumentação (ou prova) da corretude de programas
• reduzem significativamente o retrabalho inútil
– assertivas executáveis são a base para o desenvolvimento de programas auto verificáveis (self-checking)
• Texto– Pezzè, M.; Young, M.; Teste e Análise de Software; Porto Alegre, RS: Bookman;
2008, capítulo 7
– Staa, A.v.; Programação Modular; Rio de Janeiro: Campus/Elsevier; 2000, capítulo 13
2
Terminologia
• Em engenharia de software existem, infelizmente, vários nomes para a mesma coisa, ex.:
– métodos, funções, subrotinas, procedures: é tudo essencialmente a mesma coisa chamada de subrotinas
• Assertivas, contratos, pré e pós condições são a mesma coisa
– o termo contrato foi usado por Meyer ao definir a linguagem de programação orientada a objetos Eiffel em 1986
– o uso de contratos levou à definição do termo design by contract, ou projeto dirigido por contratos, ou programação dirigida por contratos
– a base é a verificação formal usando a lógica de Hoare (1969)• inspirada pelas program annotations descritas por Floyd (1967)
• Por hábito, adquirido em 1971, vou continuar a usar o termo assertiva
Fev 2018 3Arndt von Staa © LES/DI/PUC-Rio
Objetivo das assertivas
• Assertivas são essencialmente especificações formais– pré e pós condições
– invariantes da classe
– invariantes estruturais
• Têm por finalidade principal, entre outros– reduzir o retrabalho inútil
• código é escrito mais próximo do correto por construção
– apoiar a revisão de especificações, projetos e código
– apoiar a análise estática automatizada• frequentemente utilizam provadores de teoremas
– quando automatizadas, apoiar a detecção e diagnose de falhas em uso
• em componentes próprios
• em sistemas formados por serviços localizados em nuvens
Fev 2018 4Arndt von Staa © LES/DI/PUC-Rio
Ross, P.E.; “The Exterminators”; IEEE Spectrum 42(9); Los Alamitos, CA: IEEE Computer Society; 2005; pags 36-41
3
Fev 2018 5Arndt von Staa © LES/DI/PUC-Rio
Exemplo de assertiva - funcional
sqrt( x ) =:: y | 1 - < y 2/ x < 1 +
• sqrt( x ) produz y tal_que 1 - erro_tolerado < y ** 2 / x < 1 +erro_tolerado
– em que, por convenção, = 10-n, onde n é o número de dígitos significativos desejado
– Ao documentar assertivas em texto, recomenda-se utilizar a notação matemática estabelecida
– Ao documentar ou inserir assertivas no código, é necessário utilizar uma notação “digitável” restrita ao teclado disponível
– Ao documentar assertivas em linguagem natural, deve-se utilizar uma terminologia e sintaxe restrita
Fev 2018 6Arndt von Staa © LES/DI/PUC-Rio
Exemplo de assertiva - estrutural
• Exemplos
– em uma variável lista do tipo lista duplamente encadeada:
pElem lista : ? pElem->pAnt != NULL =>pElem->pAnt->pProx == pElem
ParaTodos pElem pertencentes_a lista valese pElem->pAnt != NULL entao
pElem->pAnt->pProx == pElem
4
Exemplo de assertiva – controle de especificação
O fragmento de código na linguagem Talisman 4 verifica se as ligações de existentes em um diagrama entidade relacionamento contêm um rótulo de cardinalidade
/* Objeto corrente é um diagrama entidade relacionamento */
ParaTodos InstsObjeto Faz
Conta = 0 ;
Origem = Corrente ; /* Origem é um dos elementos no diagrama */
ParaTodos LigsInstancia Faz
Conta = Conta + 1 ; /* Objeto corrente é uma ligação vinculada à Origem */
Se Nao ExisteObj( RotuloLig( Corrente ))
Entao
Titulo "Falta rótulo de cardinalidade em ligação entre: " ; NaoAvLin ;
ComObjeto Origem Faz Nome ; Fim ; NaoAvLin ; Titulo " e " ; NaoAvLin ;
ComObjeto OutraPonta( Corrente, Origem ) Faz
Nome ; Fim ; /* Exibe o nome do objeto ligado à origem */
Fim ; /* Se */
Fim ; /* ParaTodos */
Se Conta == 0
Entao
Titulo "Faltam ligações ao objeto " ; NaoAvLin ;
ComObjeto Origem Faz Nome ; Fim ;
Fim ; /* Se */
Fim ; /* ParaTodos */
Fev 2018 7Arndt von Staa © LES/DI/PUC-Rio
Linguagem desenvolvida em 1992, bem antes da UML
Objetivo das assertivas
• Quando automatizadas, têm por finalidade principal– assegurar alta detectabilidade de falhas
– apoiar a diagnose de falhas
– atuar como oráculo dos testes • viabilizam o teste automatizado usando dados gerados
• Em várias linguagens de programação podem-se avaliar as assertivas em tempo de execução usando funções que possuem a assinatura parecida com:
bool assert( bool expression )
– infelizmente cancelam a execução quando não válidas
• As assertivas executáveis podem ser complexas tornando necessárias várias funções (predicados) para avaliá-las
Fev 2018 8Arndt von Staa © LES/DI/PUC-Rio
Ross, P.E.; “The Exterminators”; IEEE Spectrum 42(9); Los Alamitos, CA: IEEE Computer Society; 2005; pags 36-41
5
Propriedades das assertivas
• Assertivas podem ser
– rigorosas: completas, coerentes, redigidas em notação formal
• utilizadas para a prova da corretude de programas (Hoare)
– leves: podem estar incompletas, podem ser texto
• permitem a argumentação da corretude– argumentação não é prova, ou seja, não garante corretude
– anotações (comentários): no programa (Floyd)
• descrevem o que deve valer em determinado ponto– Floyd usava uma notação matemática formal
– outros utilizam comentários em linguagem natural restringida
Fev 2018 9Arndt von Staa © LES/DI/PUC-Rio
• Floyd, R.W.; "Assigning meanings to programs"; Symposia on Applied Mathematics; Vol. 19; pp. 19–31; 1967
• Hoare, C A.R.; "An axiomatic basis for computer programming"; Communications of the ACM 12(10); 1969; pp 576–580
• Hall, A.; Chapman, R.; “Correctness by Construction: Developing a Commercial Secure System”; IEEE Software 19(1); Los Alamitos, CA: IEEE Computer Society; 2002; pags 18-25
Propriedades das assertivas
• Podem ser
– pontuais: redigidas em determinado ponto, estabelecem as condições que devem valer naquele ponto
– estruturais usualmente funções ou métodos que estabelecem
• as condições que devem valer para o conjunto de dados da classe e ou do objeto, ou
• as condições a serem satisfeitas por estruturas de dados formadas por diversos objetos de possivelmente diferentes classes
Fev 2018 10Arndt von Staa © LES/DI/PUC-Rio
6
Fev 2018 11Arndt von Staa © LES/DI/PUC-Rio
Propriedades das assertivas
• Uma assertiva é uma expressão condicional envolvendo dados e estados manipulados pelo fragmento de código a que diz respeito
– condições: <, <= , ==, !=, >=, >
– predicados, similares a:
• ExisteX( conjunto )
• EhTipoX( dado )
– expressões que resultem em um valor booleano
• expressões envolvem condições e/ou predicados
Fev 2018 12Arndt von Staa © LES/DI/PUC-Rio
Propriedades das assertivas
• Quando redigida como comentário, uma assertiva deve ser uma afirmação cuja validade possa ser verificada, exemplo
– “a soma dos pesos das pessoas e objetos dentro da cabina do elevador é menor ou igual a o seu limite de carga”
• é uma assertiva -> estabelece um fato a ser verificado se vale em determinado ponto do programa
• Contraste assertiva com requisito
– a forma: “antes de fechar a porta, a soma dos pesos das pessoas e objetos dentro da cabina do elevador deve ser menor ou igual a o seu limite de carga”
• é um requisito -> um desejo a ser respeitado pelo programa
• como o requisito restringe o que é legal, deveria ser acompanhado de um requisito que diz como devem ser tratadas as violações
– quando for maior deve ...
7
Fev 2018 13Arndt von Staa © LES/DI/PUC-Rio
Propriedades das assertivas
• Assertivas podem ser definidas em níveis de abstração– funções ou métodos
• usualmente pontuais
• usuais são as assertivas de entrada e as assertivas de saída– devem estar satisfeitas ao entrar e ao retornar de funções
– pré e pós condições , invariantes
– classes, módulos e componentes• assertivas invariantes da classe
– as invariantes da classe envolvem somente os atributos de um único objeto e, caso existam, os da correspondente classe (static)
• assertivas estruturais são invariantes que envolvem atributos de vários objetos possivelmente de diferentes classes
– programas, sistemas• devem estar satisfeitas para os dados de interface
– arquivos
– dados persistentes
– mensagens
– dados recebidos de ou transmitidos para equipamentos ou usuários
Propriedades das assertivas
• Assertivas são uma das formas usadas por técnicas formais leves lightweight formal methods
– são possivelmente incompletas
• devido à dificuldade de expressá-las usando notação matemática
• devido à falta de atenção do redator
• assertiva incompleta que impede a descoberta de um defeito (falso negativo) deve ser corrigida
» correção preguiçosa: é feita quando se observa um problema
– são possivelmente incorretas
• uso incorreto da notação matemática
• expressões lógicas escritas de forma incorreta
• expressões lógicas que não correspondem ao requerido
• assertiva incorreta (falso positivo) sempre deve ser corrigida– em um teste de qualidade mediana sempre se manifestam
Fev 2018 14Arndt von Staa © LES/DI/PUC-Rio
Agerholm, S.; Larsen, P.G.; “A Lightweight Approach to Formal Methods”; Proceedings FM-Trends 98 -International Workshop on Current Trends in Applied Formal Methods; Berlin: Springer; 1999; pags 168-183
8
Fev 2018 15Arndt von Staa © LES/DI/PUC-Rio
Assertivas como prevenção de defeitos
• O uso de assertivas auxilia a revisão
– a forma de raciocinar ao redigir código (comportamental) é diferente da forma de raciocinar ao redigir assertivas (declarativo), a diferença induz uma redundância de raciocínio
• essa redundância atenua os problemas relacionados com a revisão realizada pelo próprio autor
– a redundância de raciocínio é permite a revisão simultânea com o desenvolvimento
• contribui para uma significativa redução da densidade de defeitos inicial
• Logo: assertivas usualmente contribuem para aumentar a eficácia de revisões e inspeções
Fev 2018 16Arndt von Staa © LES/DI/PUC-Rio
Assertivas como prevenção de defeitos
• Enquanto se redige ou altera o código, o contínuo controle e ajuste da coerência das assertivas e do correspondente código, induz a argumentação da corretude do código
• O esforço adicional requerido para redigir e coevoluir as assertivas é em torno de 10%– modo de medir usado: percentual de linhas de código contendo
assertivas
• O esforço de teste de código redigido com assertivas usualmente é a metade do esforço quando não se usam assertivas:– modo de medir: número de defeitos encontrados, tempo médio
gasto para corrigi-los
9
Fev 2018 17Arndt von Staa © LES/DI/PUC-Rio
Benefícios esperados ao usar assertivas
• Redução do custo total em virtude de:– especificações mais precisas reduz a necessidade de
interagir com outras pessoas para descobrir o que deve ser feito
– menos retrabalho inútil
– menos defeitos remanescentes menos riscos
– melhor documentação facilita a manutenção
– facilita criar testes automatizados as assertivas são os oráculos
– redução da latência de erros reduz o esforça de diagnose da correspondente falha
Exemplo real – técnicas formais leves
Número de falhas observadas por assertivas durante testes 22
Número de falhas observadas por outros meios durante testes 5
Tempo médio para remoção de falhas, assertivas 30'
Tempo médio para remoção de falhas, outros meios 6h
Número de falhas na aceitação, assertivas 2
Número de falhas na aceitação, outros meios 0
Número de falhas nos 2 meses iniciais, leves 2
Número de falhas nos 2 meses iniciais, graves 0
Número de falhas após 2 meses de uso 0
18Arndt von Staa © LES/DI/PUC-Rio
Magalhães, J.A.P.; Staa, A.v.; Lucena, C.J.P.; “Evaluating the Recovery Oriented Approach through the Systematic Development of Real Complex Applications”; Software Practice and Experience 39(3); New York: Wiley; 2009; pags 315-330
Fev 2018
10
Exemplo: lista com cabeça
Fev 2018 19Arndt von Staa © LES/DI/PUC-Rio
pEsq pDirValor
a b c d
pOrg pCorr pFimModelo
ExemplopLista
Fev 2018 20Arndt von Staa © LES/DI/PUC-Rio
Exemplo assertiva estrutural: lista com cabeça
Controle de existência da lista
pLista != NULL
Controle da lista vazia
? (( pLista->pOrg == NULL ) || ( pLista->pFim == NULL )) =>pLista->numElem == 0
? pLista->numElem == 0 => ( pLista->pOrg == NULL ) && ( pLista->pFim == NULL )
numElem é um dado de instrumentação e que serve somente para a verificação da corretude da lista
Uma lista é vazia se e somente se origem e fim forem nulos
11
Fev 2018 21Arndt von Staa © LES/DI/PUC-Rio
Exemplo assertiva estrutural: lista com cabeça
Controle da lista não vazia
? (( pLista->pOrg != NULL ) || ( pLista->pFim != NULL )) =>pLista->numElem > 0
? pLista->numElem > 0 => ( pLista->pOrg != NULL ) &&
( pLista->pFim != NULL )
Controle do início e fim da lista não vazia
? pLista->pOrg != NULL => pLista->pOrg->pEsq == NULL
? pLista->pFim != NULL => pLista->pFim->pDir == NULL
Fev 2018 22Arndt von Staa © LES/DI/PUC-Rio
Exemplo assertiva estrutural: lista com cabeça
Verificação do corpo da lista
pElem Lista{ pLista } : /* calculado percorrendo a lista */
? pElem->pEsq == NULL => pLista->pOrg == pElem
? pElem->pEsq != NULL => pElem->pEsq->pDir == pElem
? pElem->pDir == NULL => pLista->pFim == pElem
? pElem->pDir != NULL => pElem->pDir->pEsq == pElem
pElem->EhValido( )
12
Exemplo: fragmento de assertiva executável
int SLS_SimpleList ::
Verify( ) {
int errorCount = 0 ;
...
SLS_ListElement * pElem = NULL ;
// Verify empty list
if ( ( pFirstElement == NULL )
&& ( pLastElement == NULL )
&& ( pCurrentElement == NULL )) return errorCount ; /* if */
MeuAssert( ( pFirstElement == NULL )
|| ( pLastElement == NULL )
|| ( pCurrentElement == NULL )) , ErrorIncorrectEmptyList ) ;
if ( errorCount != 0 ) return errorCount ;
// Verify first element
pElem = pFirstElement ;
MeuAssert( pElem->pPredecessor == NULL , ErrorFirstHasPredecessor ) ;
// . . .
Fev 2018 23Arndt von Staa © LES/DI/PUC-Rio
MeuAssert( cond , idMensagem )se cond for falsa, conta mais um erro e emite a mensagem idMensagem
Condição
• Condição é uma expressão cujo resultado é um booleano
– pode somente assumir os valores true ou false
– qualquer expressão válida na linguagem de programação utilizada e que avalia para um booleano pode ser uma condição
• Exemplos
– i != 0 j < 100 3 < pi
• i, i + 1 e i-- não valem, pois não são booleanos, mesmo que em algumas linguagens o inteiro 0 seja false e os demais inteiros true
– pArvore->pRaiz != NULL
• pArvore->pRaiz não vale, mesmo que algumas linguagens permitam usar if( pArvore->pRaiz ) para verificar se o ponteiro é nulo ou não
– alpha1 = arcsin( sin ( alpha )) / alpha
– ( 0.999999 < alpha1 ) && ( alpha1 < 1.000001 )
Fev 2018 24Arndt von Staa © LES/DI/PUC-Rio
controle usando tolerância
13
Fev 2018 25Arndt von Staa © LES/DI/PUC-Rio
Conjunção, expressão “e”
1) condição1 && condição2 && ... && condiçãon
2) condição1 condição2 ... condiçãon
3) condição1 , condição2 , ... , condiçãon
4) condição1
condição2
...
condiçãon
– as quatro expressões são equivalentes
– para que a expressão seja verdadeira, todas as condições 1, 2, ... n devem ser verdadeiras
– evite a forma 2, pois confunde com o operador “^” (ou exclusivo bit a bit) de C / C++
Fev 2018 26Arndt von Staa © LES/DI/PUC-Rio
Disjunção, expressão “ou”
1) condição1 || condição2 || ... || condiçãon
2) condição1 condição2 ... condiçãon
– as duas formas são equivalentes
– para que a expressão seja verdadeira uma ou mais das condições 1, 2, ... n devem ser verdadeiras
– evite a forma 2, por analogia à restrição do uso de “” nas expressões conjuntivas
• além do mais confunde com a letra ‘v’ que, para analisadores léxicos é um nome
14
Fev 2018 27Arndt von Staa © LES/DI/PUC-Rio
Disjunção exclusiva, expressão “xor”
1) condição1 xor condição2 xor ... xor condiçãon
– para que a expressão seja verdadeira exatamente uma das condições 1, 2, ... n deve ser verdadeira
• exatamente: uma e somente uma
• xor: exclusive or
Fev 2018 28Arndt von Staa © LES/DI/PUC-Rio
Negação
• ! Condição
– se Condição for verdadeira, a expressão será falsa
– se Condição for falsa, a expressão será verdadeira
• Encontram-se por vezes os símbolos: ‘~’ ou ‘’ para designar negação
15
Fev 2018 29Arndt von Staa © LES/DI/PUC-Rio
Implicação, se
1) se premissa então consequente
2) ? premissa => consequentea expressão ? => ’ simplifica a análise sintática, em especial humana a expressão => ’ somente é reconhecida depois de encontrar o "=>",
se for longo isso pode gerar confusão
se premissa for verdadeira e a consequente também for verdadeira, a expressão será verdadeira
se premissa for verdadeira e a consequente for falsa, a expressão será falsa
se premissa for falsa, a expressão será verdadeira independente da consequente
• na realidade se premissa for falsa a expressão passa a ser irrelevante – a partir de uma premissa falsa qualquer conclusão vale
Fev 2018 30Arndt von Staa © LES/DI/PUC-Rio
Implicação, se
• evite else, redija a implicação com a premissa negada, exemplo
!( premissa ) => consequente
– similar a um “guarded command” (comando com guarda)
• evite aninhamentos de ifs, redija a expressão condicional completa
• evite a dependência da precedência usual da linguagem usada, redija a expressão condicional parentetizada
16
Se e somente se
1. condição_a sse condição_b
2. ? condição_a <=> condição_b
• Para a expressão ser verdadeira precisa-se mostrar que:
– se condição_a == V então condição_b == V
– se condição_a == F então condição_b == F
– se condição_b == V então condição_a == V (recíproca)
– se condição_b == F então condição_a == F
Fev 2018 31Arndt von Staa © LES/DI/PUC-Rio
Fev 2018 32Arndt von Staa © LES/DI/PUC-Rio
Conjuntos
• { A1 , A2 , ... , An }
– em que A1, A2, ... , An são elementos, objetos, ou referências a objetos
17
Fev 2018 33Arndt von Staa © LES/DI/PUC-Rio
Conjuntos
• Nome ou Nome{ refEstrutura }
– é o conjunto de todos os elementos da estrutura Nome,
– caso exista a chave refEstrutura
• Nome é o tipo e refEstrutura identifica a instância
– sugestão:
• no caso C referencie sempre a cabeça da estrutura
• no caso OO procure ancorar toda a estrutura em um objeto cabeça
– o tipo da estrutura deve estar implícito no nome.
• se não estiver pode-se usar Tipo :: Nome{ refEstrutura }
Fev 2018 34Arndt von Staa © LES/DI/PUC-Rio
Conjuntos
• { regra de formação do conjunto }
– a regra é uma expressão,
• ex. uma expressão envolvendo um quantificador
• ex. uma gramática, que indica a lei de formação dos elementos do conjunto
– exemplos
{ pElem Lista{ pLista } | pElem->pEsq == NULL }
< Inteiros > ::= $digito 0 – 9 [ $digito ] ; produção de uma gramática
{ i | i Inteiros } todos os elementos pertencentes à gramática
definido por
< x > : x é um não terminal, ou uma gramática (i.e. o não terminal origem das produções)
18
Fev 2018 35Arndt von Staa © LES/DI/PUC-Rio
Quantificadores
• ParaTodos , ou
• Pertence , ou
• Vale , ou :
• TalQue , ou |
• Exemplo:– pElem Lista{ pLista } : condição1 , condição2 , ...
• para todos os elementos pElem pertencentes à lista pLista valem as condições: condição1 , condição2 , ...
• use pElem caso se trate de um ponteiro para o elemento ou refElem caso se trate de uma referência explícita
– obs.: em Java todos os objetos são implicitamente referenciados, neste caso use elem
– i | (0 <= i < n ) : condição1 , condição2 , ...• para todos os i tal que i esteja no intervalo [ 0 .. n ) valem as
condições: condição1 , condição2 , ...
Fev 2018 36Arndt von Staa © LES/DI/PUC-Rio
Quantificadores
• Exemplo:
– pElem Lista{ pLista } | condiçãoA , condiçãoB : condição1 , condição2 , ...
– pElem Lista{ pLista } | pElem->pEsq != NULL : pElem->pEsq->pDir == pElem
– pElem Lista{ pLista } | pElem->pDir != NULL : pElem->pDir->pEsq == pElem
19
Fev 2018 37Arndt von Staa © LES/DI/PUC-Rio
Quantificadores
• Existe ou
• TalQue ou |
• Para estes valem ou :
• Exemplo
– pElem Lista{ pLista } | condição1 && condição2
• existe pelo menos um elemento pElem, pertencente à lista pLista, tal que as condições condição1 e condição2 sejam verdadeiras
• Problema com Existe: pode existir nenhum, pode existir exatamente um, podem existir vários
– precisa-se considerar cada um desses três casos
Fev 2018 38Arndt von Staa © LES/DI/PUC-Rio
Cardinalidade de conjunto
• || conjunto || cardinalidade – número de elementos doconjunto
• card( conjunto ) cardinalidade em notação que nãoconfunde com o operador ou lógico “||”
• VAZIO ou conjunto vazio
• ? card( { pElem Lista{ pLista } | pElem->pEsq == NULL } )!= 1 => erro
• ? card( { pNo Arvore{ pArvore } | pNo == pArvore->pNoCorrente } ) != 1 => erro
o que querem dizer as expressões acima?
20
Fev 2018 39Arndt von Staa © LES/DI/PUC-Rio
Variáveis e atribuição lógicas
• Seja Variávela = Variávelb
ou
• Seja Variávela = Expressão
– variáveis lógicas que existem somente para fins de processamento de condições, exemplo:
• pArv->numNos – esta variável não faz parte do modelo da árvore, entretanto poderia fazer e é facilmente calculável ao efetuar operações sobre árvores
– o tipo da variável pode ser qualquer,
• se não for booleano, a variável precisará ser utilizada em uma condição
• se for booleano, a variável pode ser a própria condição
– variáveis e atribuições lógicas não devem ser necessárias para o processamento produtivo, dessa forma podem corresponder a código compilado condicionalmente
Fev 2018 40Arndt von Staa © LES/DI/PUC-Rio
Funções lógicas
• nome_da_função ( lista_de_parâmetros ) ::= expressão
– ::= leia-se “definida como”
– a expressão deve envolver todos os parâmetros
– a função não deve gerar efeitos colaterais
• alterações de variáveis lógicas somente podem ser realizadas por atribuições lógicas específicas
– funções lógicas não devem ser necessárias para o processamento produtivo, dessa forma podem corresponder a código compilado condicionalmente
– Exemplo
bissexto( a ) ::= a div 400 ||
( a div 4 && !( a div 100 ))a div b: retorna true se a for divisível por b, ex. ( a>0 && b>0 ? a%b==0 : false )
No calendário Gregoriano (1582): são bissextos os anos divisíveis por 400, dos restantes não são bissextos os divisíveis por 100, dos restantes agora são bissextos os divisíveis por 4. Segundo a conta o ano "médio" terá 365 + 97 / 400 dias = 365,2425 dias. O ano Tropical medido é aproximadamente de 365,24219 dias, assim o calendário Gregoriano produz um excesso de um dia a cada 3300 anos.
21
Controle de tempo, proposta
• Em tempo de execução o controle de tempo requer uma função que retorne o relógio corrente
– C/C++ a expressão clock( ) / CLOCKS_PER_SEC retorna tempo decorrido desde o início da execução em segundos, com uma fração de possivelmente centésimos de segundo dependendo da máquina, do compilador e do modo de otimização. Problema: falta de precisão e portatilidade
• Com essa expressão pode-se marcar o início e o final da execução e verificar se o tempo decorrido está dentro das restrições esperadas. Problemas:
– latência / precisão-do-relógio precisa ser grande (>100?)
– multiprogramação
• Assertiva temporal que mede o tempo consumido por P
latency( P( argumentos) ) < tempo limite
Fev 2018 41Arndt von Staa © LES/DI/PUC-Rio
Heisenbug
Rocha, P.G.C.; Um mecanismo baseado em logs com meta-informações para a verificação de contratos em sistemas distribuídos; Dissertação de Mestrado, Departamento de Informática, PUC-Rio; Rio de Janeiro; 2014
Apêndice
Fev 2018 42Arndt von Staa © LES/DI/PUC-Rio
22
pFilho Valor
pRaiz pCorrente
pPaipCorr
m
a
b dc
g
h i j k l
fe
pEsq pDir
Exemplo assertiva estrutural: árvore n-ária 1 / 4
árvore memoriza o filho corrente, facilita a exploração de toda a árvore
Fev 2018 43Arndt von Staa © LES/DI/PUC-Rio
Fev 2018 44Arndt von Staa © LES/DI/PUC-Rio
Exemplo assertiva estrutural: árvore 2 / 4
Cabeça da árvore é pArv != NULL
• Sse a árvore estiver vazia: pArv->pRaiz == NULL e pArv->pCorrente == NULL
• Sse a árvore não estiver vazia:
– pArv->pRaiz aponta para o nó raiz da árvore
– pArv->pCorrente aponta para um dos nós da árvore
Outra redação:
?( pArv->pRaiz == NULL || pArv->pCorrente == NULL ) =>
pArv->numNos == 0
?pArv->numNos == 0 => pArv->pRaiz == NULL &&pArv->pCorrente == NULL
?pArv->numNos != 0 => pArv->pRaiz != NULL && pNo Arvore{ pArv } | pNo == pArv->pCorrente
pArv->numNos é um atributo necessário para as assertivas, mas não necessariamente em produção
23
Fev 2018 45Arndt von Staa © LES/DI/PUC-Rio
Exemplo assertiva estrutural: árvore 3 / 4
Corpo da árvore:
pNo Arvore{ pArv } :
? pNo->pPai == NULL => pArv->pRaiz == pNo &&pNo->pEsq == NULL && pNo->pDir == NULL
? pNo->pPai != NULL => pElem Lista{ pNo->pPai->pFilho } |pElem == pNo
? pNo->pFilho == NULL => pNo->pCorr == NULL
? pNo->pFilho != NULL => ( pNo->pFilho->pEsq == NULL ) &&
( pFil Lista{ pNo->pFilho } : pFil->pPai == pNo ) &&
( pFil Lista{ pNo->pFilho } | pNo->pCorr == pFil )
Fev 2018 46Arndt von Staa © LES/DI/PUC-Rio
Exemplo assertiva estrutural: árvore 4 / 4
pNo Arvore{ pArv } : /* continuação */
? pNo->pEsq == NULL && pNo->pPai == NULL =>
pArv->pRaiz == pNo
? pNo->pEsq == NULL && pNo->pPai != NULL =>
pNo->pPai->pFilho == pNo
? pNo->pEsq != NULL => pNo->pEsq->pDir == pNo
? pNo->pDir == NULL => true
? pNo->pDir != NULL => pNo->pDir->pEsq == pNo
? pNo->pDir != NULL => pNo->pPai == pNo->pDir->pPai
• sempre assegure que sejam consideradas todas as partições da expressão usada como premissa
• no caso de dúvida crie uma tabela de decisão para fins de verificação
24
Fev 2018 47Arndt von Staa © LES/DI/PUC-Rio
Assertivas executáveis
• São instrumentos de detecção de erros, i.e. falhas
• Reduzem o esforço para diagnosticar falhas
– a instrumentação pode ser inserida de modo que a latência de observação dos erros seja pequena
– o relato de falha (log) pode conter os valores dos dados críticos no momento da detecção
• Viabilizam a geração automática de casos de teste
– podem servir de oráculos dinâmicos
– viabilizam o teste baseado na geração de dados aleatórios
• São necessárias para desenvolver artefatos robustos
– permitem a criação de programas auto-verificantes (“self-checking”)
– observam erros quase no momento em que são gerados, evitando danos substanciais
Exemplos de assertivas executáveis
• Em uma lista, mover o índice de elemento corrente numMoveelementos em direção à origem (numMove < 0), ao final (numMove > 0), ou nada (numMove == 0)
int LST_List :: MoveCurrElement( int numMove )
{
// Assertiva de entrada
#ifdef _DEBUG
EXC_ASSERT( inxCurrElem >= -1 ) ;
EXC_ASSERT( inxCurrElem == -1 ? pCorr == NULL : true ) ;
EXC_ASSERT( inxCurrElem == 0 ? pPrev == NULL : true ) ;
EXC_ASSERT( inxCurrElem < numElem ) ;
EXC_ASSERT( inxCurrElem == numElem – 1 ? pProx == NULL :
true ) ;
int inxCurrElemEntrada = inxCurrElem ;
#endif
Fev 2018 48Arndt von Staa © LES/DI/PUC-Rio
índice corrente será < 0 sse o “elemento” corrente estiver antes da origem da lista
Necessário para mais tarde saber o valor ao entrar
obviamente deveria existir uma relação envolvendo pCorr e inxCurrElem
25
Exemplos de assertivas executáveis
// Assertiva de saída
#ifdef _DEBUG
EXC_ASSERT( inxCurrElem >= -1 ) ;
EXC_ASSERT( inxCurrElem == -1 ? pCorr == NULL : true ) ;
EXC_ASSERT( inxCurrElem == 0 ? pPrev == NULL : true ) ;
EXC_ASSERT( inxCurrElem < numElem ) ;
EXC_ASSERT( inxCurrElem == numElem – 1 ? pProx == NULL :
true ) ;
EXC_ASSERT( inxCurrElem >= max( -1 ,
inxCurrElemEntrada + numMove ) ;
EXC_ASSERT( inxCurrElem <= min( numElem -1 ,
inxCurrElemEntrada + numMove ) ;
#endif
Fev 2018 49Arndt von Staa © LES/DI/PUC-Rio
Observação: Uma parte da assertiva de entrada é igual a uma parte da de saída, embora os valores possam variar ao operar sobre a estrutura, logo essa parte da assertiva é uma invariante estrutural
Efeito da operação
Fev 2018 50Arndt von Staa © LES/DI/PUC-Rio
FIM