Aula 4: Especificações de Procedimentos
4.1. Introdução
Nesta aula, iremos analisar o papel das especificações de métodos. Especificações são o elo
do trabalho de equipe. É impossível delegar-se responsabilidades de implementação de um
método sem uma especificação. A especificação funciona como um contrato: o
desenvolvedor é responsável por satisfazer o contrato, e o cliente que utiliza o método pode
se basear no compromisso definido pelo contrato. De fato, iremos ver que assim como
verdadeiros contratos legais, as especificações determinam responsabilidades para ambas as
partes: enquanto que a especificação possui condições a serem respeitadas, o cliente que se
baseia nestas especificações também tem suas responsabilidades.
Muitos dos mais desagradáveis bugs dos programas surgem em função de interpretações
errôneas a respeito do comportamento das interfaces. Embora todo programador tenha
especificações em mente, nem todos as deixam claramente definidas de maneira escrita.
Como resultado, diferentes programadores de uma equipe têm diferentes especificações em
mente. Quando o programa falha, é difícil determinar onde o erro está. Especificações
precisas no código ajudam a distribuir a responsabilidade (a fragmentos de código, não a
pessoas!) e podem poupar você da agonia de montar o quebra-cabeça a respeito da decisão
de onde uma correção deve ser feita.
Especificações são boas para o cliente que utiliza um método, pois elas poupam o cliente da tarefa
de ler o código. Se você não está convencido de que ler a especificação (ou spec na forma
abreviada) é mais fácil do que ler o código, então dê uma olhada em algumas especificações do Java
padrão e as compare com o código fonte que as implementa. Vector, por exemplo, no package
java.util possui um spec bastante simples enquanto que seu código possui uma alta complexidade.
Especificações são boas para o desenvolvedor de um método, pois elas dão liberdade para se alterar
a implementação sem que seja necessário avisar aos clientes. Especificações podem tornar o código
mais rápido também. Às vezes, uma especificação fraca torna possível uma implementação bem
mais eficiente. Em particular, uma dada condição de uma spec pode controlar certos estados nos
quais um método pode estar envolvido, de forma que uma custosa checagem desta condição não é
mais necessária em função da sistemática que o uso das especificações proporciona.
Esta aula está relacionada com nossa discussão a respeito de desacoplamento e de dependências,
44
tópicos que foram vistos nas últimas duas aulas. Lá, estávamos preocupados apenas com a questão
da existência de uma dependência. Aqui, estaremos investigando a questão a respeito de qual forma
a dependência deve ter. Expondo apenas a especificação de um procedimento, seus clientes serão
menos dependentes do procedimento e, portanto, haverá menor tendência de necessidade de
alterações quando os procedimentos utilizados forem modificados.
4.2. Equivalência Comportamental
Considere estes dois métodos. Eles são os mesmos, ou são diferentes?
static int findA (int [] a, int val) {
for (int i = 0; i < a.length; i++) {
if (a[i] == val) return i;
}
return a.length;
}
static int findB (int [] a, int val) {
for (int i = a.length -1 ; i > 0; i--) {
if (a[i] == val) return i;
}
return -1;
}
É claro que o código é diferente, portanto, neste sentido pode-se dizer que os métodos são
diferentes. Nossa questão, no entanto, é se um deles poderia substituir a implementação do outro.
Estes métodos não possuem apenas diferentes codificações; na verdade, eles possuem diferentes
comportamentos:
· quando val não é encontrado no array passado como argumento, findA retorna o comprimento do
array passado enquanto que findB retorna -1;
· quando val aparece duas vezes dentro do array passado como argumento, findA retorna o menor
índice da ocorrência de val enquanto que findB retorna o maior.
Mas quando val é encontrado exatamente uma vez dentro do array, os dois métodos se comportam
da mesma forma. Pode ser que, para os outros dois casos acima, os clientes nunca irão se basear no
comportamento apresentado pelo método. Desta forma, a noção de equivalência está nos olhos de
quem vê, isto é, o cliente. Para que seja possível substituir uma implementação por outra, e saber
quando isto é aceitável, precisamos de uma especificação que defina exatamente do que o cliente
depende.
45
Neste caso, nossa especificação pode ser
requires:
effects:
val ocorre em a
retorna um resultado tal que a[result] = val
4.3. Estrutura de Especificação
A especificação de um método consiste de várias cláusulas:
· uma pré-condição, indicada pela palavra chave, ou keyword, requires;
· uma pós-condição, indicada pela keyword effects;
· uma condição estrutural, indicada pela keyword modifies.
Explicaremos estas cláusulas uma por vez. Para cada uma, vamos explicar o que a cláusula
significa, e no que uma cláusula ausente implica. Mais tarde, iremos analisar alguns macetes muito
convenientes que permitem que uma linguagem menos formal possa ser definida através de tipos
especiais de cláusulas.
A pré-condição é uma obrigação a ser satisfeita pelo cliente (isto é, aquele que chama o método)
antes que ele possa fazer a chamada. É uma condição a respeito do estado do sistema no momento
quando o método é invocado. Se a pré-condição não é satisfeita antes da chamada, a implementação
do método fica livre para fazer qualquer coisa (incluindo nunca retornar da execução, jogar uma
exceção, retornar resultados arbitrários, realizar modificações arbitrárias, etc).
A pós-condição é uma obrigação do desenvolvedor do método. Se a pré-condição está satisfeita no
momento da invocação do método, o método é obrigado a obedecer a pós-condição, retornando,
portanto, valores apropriados, jogando exceções especificadas, modificando ou não modificando
objetos e assim por diante.
A condição estrutural está relacionada com a pós-condição. Ela permite especificações mais
sucintas. Sem uma condição estrutural, seria necessário descrever como todos os objetos que podem
ser acessados podem ser modificados, e como não podem. Mas, normalmente, apenas alguns
objetos são modificados. A condição estrutural identifica quais objetos podem ser modificados. Se
dissermos ‘modifies x’, isto quer dizer que o objeto x, o qual entende-se que possa ser modificado,
poderá ser modificado, mas apenas x e nenhum outro objeto, mesmo que não tenha sido
mencionado. Portanto, a cláusula estrutural, ou cláusula modifies como é chamada, é uma
afirmação, uma notificação, a respeito dos objetos que não são mencionados. Para aqueles que são
mencionados, a modificação de seus estados é possível, mas não necessária; para aqueles que não
são mencionados, não pode haver modificação.
Cláusulas omissas possuem interpretações particulares. Se você omitir a pré-condição, a ela é
46
atribuído o valor padrão ‘verdadeiro’. O que quer dizer que qualquer estado do sistema, durante
uma invocação, satisfaz a pré-condição, não havendo obrigação de realização de qualquer tipo de
verificação por parte de quem realiza a chamada. Neste caso, diz-se que o método é total. Se a précondição não é verdadeira, diz-se que o método é parcial, pois só funciona em alguns estados do
sistema.
Se a condição estrutural for omitida, o padrão assumido é ‘não modifique nada’. Em outras
palavras, o método não faz qualquer alteração em nenhum objeto.
Omitir a pós-condição não faz sentido e nunca é feito desta maneira.
4.4. Especificação Declarativa
Informalmente, existem dois tipos de especificações. Especificações operacionais fornecem uma
série de passos que o método realiza; descrições em pseudocódigo são operacionais, por exemplo.
Especificações declarativas não fornecem detalhes de passos intermediários. Ao invés disso, elas
apenas fornecem propriedades do resultado final, e como este resultado está relacionado com o
estado inicial.
Quase sempre, especificações declarativas são preferíveis. Geralmente elas são mais curtas, mais
fáceis de serem compreendidas e, o mais importante, elas não expõem, inadvertidamente, detalhes
de implementação sobre os quais um cliente pode se basear (e perceber mais tarde que estes
detalhes não são mais válidos, quando a implementação é alterada). Por exemplo, se queremos
permitir ambas as implementações do método find, do exemplo do início da aula, nós não vamos
querer que seja mencionado no spec que o método ‘sobe pelo array até que encontre val’, pois, além
de ser vago, este espec sugere que a busca é feita do menor para o maior índice e que o menor dos
índices será retornado, o que, talvez, a pessoa que definiu a especificação não pretendia.
Aqui temos alguns exemplos de especificação declarativa. A classe StringBuffer fornce objetos que
são como objetos String, mas que podem ser modificados. Os métodos de StringBuffer modificam
o objeto ao invés de criar novos : eles são modificadores, enquanto que os métodos da classe String
são produtores. O método reverse inverte uma string. Aqui apresentamos como este método é
especificado na API Java:
public StringBuffer reverse()
// modifies: this
// effects: Seja n o comprimento da seqüência de caracteres anterior, a que está contida
// no string buffer antes da execução do método reverse. Então, o caractere na posição de
//índice k na nova seqüência de caracteres é igual ao caractere na posição n-k-1 da
47
//seqüência de caracteres anterior.
Perceba que a pós-condição não dá qualquer detalhe sobre como a inversão é realizada; ela apenas
fornece uma propriedade que relaciona a seqüência de caracteres antes e depois. (Omitimos parte da
especificação, falando nisso: o valor de retorno é o próprio objeto StringBuffer.) De maneira um
pouco mais formal, podemos escrever:
effects:
length (this.seq) = length (this.seq’)
para todo k: 0..length(this.seq)-1 | this.seq’[k] = this.seq[length(this.seq)-k-1]
Aqui, utilizei a notação this.seq para expressar o valor da seqüência de caracteres deste objeto após
a execução. O texto do curso utiliza a keyword post como uma abreviação para este mesmo
propósito. Não há pré-condição, portanto o método deve funcionar também quando o StringBuffer
está vazio; neste caso, ele irá deixar o buffer intocado.
Um outro exemplo, desta vez da classe String. O método startsWith testa se uma string é iniciada
por uma dada substring.
public boolean startsWith(String prefix)
// Testa se a string é iniciada pelo prefixo especificado.
// effects:
// if (prefix = null) throws NullPointerException
// else returns true if existe uma sequência tal que (prefix.seq ^ s = this.seq)
Assumi que os objetos String, assim como os objetos StringBuffer, possuem um campo (seq) de
especificação que modela a seqüência de caracteres. O símbolo de acento circunflexo é o operador
de concatenação, assim, a pós-condição determina que o método retorna true se há qualquer sufixo
que quando concatenado com o argumento passado como parâmetro, resulta em uma seqüência de
caracteres igual ao do objeto String em questão, isto é, this. A ausência da cláusula modifies indica
que nenhum outro objeto é modificado. Como String é um tipo que não pode ser modificado,
nenhum de seus métodos irá possuir cláusula modifies.
Outro exemplo do objeto String, o métdo substring(int i) retorna a substring cujo primeiro caractere
está na posição i (lembrando que a primeira posição é a posição zero):
public String substring(int i)
// effects:
// if i < 0 or i > length (this.seq) throws IndexOutOfBoundsException
// else returns r tal que
// para alguma seqüência s | length(s) = i && s ^ r.seq = this.seq
48
Esta especificação mostra como uma pós-condição mais matemática às vezes pode ser mais fácil de
ser compreendida do que uma descrição informal. Melhor do que ficar falando sobre se i é o índice
inicial, se ele vem logo após a substring retornada, etc, nós simplesmente decompomos a string em
duas partes: um prefixo de comprimento i, e a string retornada.
Nosso exemplo final mostra como uma especificação declarativa pode expressar o que muitas vezes
é chamado de ‘não-determinismo’, mas que é mais bem denominado ‘sub-determinismo’. Não
fornecendo detalhes suficientes que permitam ao cliente deduzir o comportamento do código em
todos os casos, a especificação torna a implementação mais fácil. O termo não-determinismo sugere
que a implementação deva exibir todas os possíveis comportamentos que satisfaçam a
especificação, o que não é o caso.
Existe uma classe denominada BigInteger no package java.math cujos objetos são do tipo inteiro
de tamanho ilimitado. A classe possui um método parecido com isso:
public boolean maybePrime ()
// effects: if o BigInteger é composto, returns false
Se este método retornar false, o cliente sabe que o inteiro não é primo. Mas se retorna true, o inteiro
pode ser primo ou composto. Desde que o método retorne false uma proporção razoável de vezes,
ele é útil. De fato, como a API Java determina: ‘o método recebe um argumento que é uma medida
de incerteza que a pessoa que está invocando o método está disposta a tolerar. O tempo de execução
deste método é proporcional ao valor de seu parâmetro’. Nós não iremos nos preocupar com
questões probabilísticas neste curso; apenas mencionamos este spec para mostrar que ele não
determina qual será o resultado da execução do método e, mesmo assim, é útil para seus clientes.
Aqui temos um exemplo de uma especificação verdadeiramente indeterminada. No padrão de
projeto Observer, um conjunto de objetos conhecidos como ‘observadores’ são informados de
alterações ocorridas em um dado objeto denominado ‘sujeito’. O sujeito irá pertencer a uma classe
que é subclasse de java.util.Observable. Na especificação de Observable, há um campo de
especificação1 denominado observadores, que mantém o conjunto de objetos observadores. Esta
classe fornece métodos para adicionar um observador:
public void addObserver(Observer o)
// modifies: this
// effects: this.observers’ = this.observers + {o}
1
O conceito de campos de especificação será introduzido na próxima aula.
49
O símbolo ‘+’ é utilizado como operador de união entre conjuntos e, para notificar os observadores
de uma alteração no estado do sujeito, existe o método:
public void notifyObservers()
// modifies: os objetos em this.observers
// effects: chama o.notify em cada observador o do conjunto this.observers
A especificação de notify não indica em qual ordem os observadores são notificados. A ordem
escolhida pode afetar o comportamento global do programa, mas tendo escolhido modelar os
observadores como um conjunto, não há como especificar uma ordem.
4.5. Exceções e Pré-condições
Uma questão óbvia de projeto é: utilizar ou não utilizar uma pré-condição e, se caso a decisão seja
utilizar uma pré-condição, a questão é se ela deve ser checada, ou não. É crucial compreender que
uma pré-condição não requer que a checagem seja feita. Pelo contrário, o uso mais comum de précondições é exigir que uma propriedade seja satisfeita antes da chamada, justamente porque seria
muito difícil ou custoso checá-la dentro da implementação do método.
Como mencionado acima, uma pré-condição não-trivial estabelece que o método é parcial. O que é
inconveniente para os clientes, pois eles têm que se certificar que não estão chamando o método
estando o sistema em um estado não propício (que viola a pré-condição); se o fizerem, não há meios
previstos para se recuperar do erro. Portanto, usuários de métodos não gostam de pré-condições, e
por esta razão os métodos de uma biblioteca, normalmente, serão totais, isto é, sem pré-condições.
É por causa disso que a API de classes Java, por exemplo, invariavelmente joga exceções quando
argumentos são inapropriados, o que torna mais robusto o programa que utiliza seus métodos e que
poupa os cliente de fazerem checagens. Estas checagens são realizadas dentro da implementação
que joga uma exceção caso alguma propriedade exigida não seja satisfeita.
Às vezes, no entanto, a pré-condição permite que se escreva código mais eficiente e capaz de
prevenir problemas. Por exemplo, em uma implementação de uma árvore binária, pode-se ter um
método private que realiza o balanceamento da árvore. O método deve manipular o caso em a
invariante que determina que a árvore deve estar ordenada não é satisfeita? Obviamente que não,
pois é muito caro para se realizar tal checagem. Dentro da classe que implementa a árvore, é
razoável que se assuma que a invariante é verdadeira. Nós iremos generalizar este conceito quando
falarmos de invariantes de representação em uma aula próxima.
A decisão de se utilizar uma pré-condição fica a cargo do julgamento do engenheiro. Os fatores
principais a serem considerados são o custo de checagem (na escrita e execução do código), e o
50
escopo do método. Se ele é chamado apenas localmente em uma classe, a pré-condição pode ser
satisfeita checando-se cuidadosamente todos os locais de chamadas do método. Mas se o método é
público, e utilizado por outros desenvolvedores, não seria muito sensato utilizar uma pré-condição.
Às vezes, não é possível checar uma condição sem fazer com que um método fique
insuportavelmente lento, e uma pré-condição normalmente é necessária neste caso. Na biblioteca
padrão do Java, por exemplo, os métodos de busca binária das classes Arrays requerem que o array
fornecido como argumento esteja ordenado. A checagem a respeito da ordenação do array iria
destroçar com o propósito da busca binária: que é obter um resultado em tempo logarítmico, ao
invés de fazê-lo em tempo linear.
Mesmo que se decida usar uma pré-condição, pode ser possível inserir checagens úteis que irão
detectar, pelo menos às vezes, que a pré-condição foi violada. Estas violações são detectadas pelas
denominadas ‘certificações em tempo de execução’: informações geradas pelo programa em tempo
de execução na forma de exceções. Muitas vezes você não irá checar a pré-condição explicitamente
no início, mas irá descobrir o erro durante a computação. Por exemplo, no balanceamento da árvore
binária, você pode checar se os filhos de um dado nó da árvore estão ordenados apropriadamente,
apenas quando, realizando outro processamento, visitar este nó.
Caso perceba-se que uma pré-condição é violada, você deve jogar uma exceção informando a
respeito do que não foi checado. O cliente não estará preparado para manipular tal exceção, o que
deverá ser feito quando recebê-la. A prática de se jogar exceções não é mencionada nas
especificações, no entanto, informações a respeito podem estar presentes em notas na
implementação.
4.6. Macetes
Existem truques convenientes que tornam mais fácil escrever especificações. Quando um método
não modifica nada, especificamos o valor de retorno na cláusula returns. Se uma exceção é jogada,
a condição e a exceção são informadas em uma cláusula throws. Por exemplo, ao invés de
public boolean startsWith(String prefix)
// effects:
// if (prefix = null) throws NullPointerException
// else returns true if existir uma sequência s tal que (prefix.seq ^ s = this.seq)
podemos escrever
public boolean startsWith(String prefix)
51
// throws: NullPointerException if (prefix = null)
// returns: true if existir uma seqüência s tal que (prefix.seq ^ s = this.seq)
Esta forma de se expressar a especificação de um método implica que nenhuma modificação ocorre.
Há uma ordenação implícita na qual as condições são avaliadas: qualquer cláusula throws é
considerada na ordem em que aparecem, e, em seguida, são avaliadas as cláusulas returns. O que
nos permite omitir a parte else das sentenças if-then-else.
O gerador de especificações do curso 6170 é baseado no gerador JavaDoc e produz, portanto,
especificações no estilo da API Java. Isto nos permite utilizar as cláusulas que discutimos aqui, e
que têm sido um padrão na comunidade de projetos por várias décadas, junto com as cláusulas
throws e returns. Nós não iremos utilizar a cláusula de parâmetros do JavaDoc: além de ser
incorporada pela cláusula de pós-condição, normalmente ela é muito trabalhosa para escrever.
4.7. Ordenação da Especificação
Suponha que você queira substituir um método por outro. Como você compara as especificações?
Uma especificação A é, no mínimo, tão boa quanto uma especificação B se:
· a pré-condição de A não é tão rígida quanto a de B
· a pós-condição de A não é menos rígida do que a de B, para os estados que satisfazem a précondição de B.
Estas duas regras englobam diversas idéias. Elas significam que você pode sempre tornar menos
rígida uma dada pré-condição; requerendo menos exigências de um cliente você nunca irá perturbálo. Você pode sempre reforçar a pós-condição, o que significa que você pode ‘fazer mais
promessas’. Por exemplo, nosso método maybePrime pode ser substituído, em qualquer contexto,
por um método isPrime que retorna true se e apenas se o número inteiro em questão é primo. E
onde a pré-condição é falsa, você pode fazer o que desejar. Se acontecer da pós-condição
especificar o resultado do método para um estado que viola a pré-condição, você pode ignorá-la,
pois, de qualquer forma, a saída não é garantida.
Estes relacionamentos entre especificações serão importantes quando analisarmos as condições sob
as quais a prática de subclasses funciona corretamente (em nossa aula sobre derivação e subclasses).
4.8. Julgando Especificações
O que torna bom um método? Projetar um método significa, fundamentalmente, escrever uma
especificação. Não existem regras infalíveis, mas existem algumas diretrizes:
· A especificação deve ser coerente: ela não deve ter um monte de casos diferentes. Sentenças if
52
aninhadas em profundidade são um sinal de problema, como também o são flags booleanas
introduzidas como argumentos.
· Os resultados de uma chamada devem ser informativos. A classe do Java denominada
HashMap possui um método put que recebe uma chave e um valor, e retorna um valor
anteriormente recebido caso aquela chave já tenha sido mapeada, ou null caso contrário.
HashMaps permitem que referências para null sejam armazenadas, de forma que um resultado
null é de difícil interpretação.
· A especificação deve ser rígida o suficiente. Não há sentido em se jogar uma exceção que foi
checada para um argumento cujo valor não satisfaz a pré-condição, mas que sofreu alterações
arbitrárias no seu valor no decorrer da execução. Um cliente não será capaz de determinar
quais alterações foram realizadas.
· A especificação deve ter uma rigidez mínima. Um método que recebe uma URL e que retorna
uma conexão, claramente não pode prometer que sempre terá sucesso na execução.
4.9. Resumo
Uma especificação funciona como um firewall crucial entre o desenvolvedor do procedimento e seu
cliente. Ela torna possível o desenvolvimento em paralelo: o cliente está livre para escrever código
utilizando o procedimento sem ver seu código fonte, e o desenvolvedor está livre para escrever
código que implementa o procedimento sem saber como ele será utilizado. Especificações
declarativas são as mais úteis na prática. Pré-condições tornam a vida mais difícil para o cliente,
mas, aplicadas de maneira prudente, são uma ferramenta vital do repertório do projetista de
software.
53