Os dois exemplos que vimos na secção anterior ilustram situações extremamente comuns em programação – a necessidade de generalizar ações semelhantes, identificando as partes comuns e as que variam:
ExemploPolimorfismoParametros
construímos dois métodos que generalizaram dois conjuntos de instruções; cada método define uma sequência de ações sobre um dado objeto do tipo Jogo
, parâmetro do método; este pode ser instanciado por uma referência a um objeto de qualquer subtipo de Jogo
. ExemploPolimorfismoArray
temos uma mesma sequência de instruções aplicada sobre dois objetos de tipos diferentes; como estes objetos têm um supertipo comum – Jogo
– podem ser acedidos através de variáveis desse tipo – meusJogos[0]
e meusJogos[1]
.
Como o tipo declarado dos objetos é Jogo
, ainda que o seu tipo concreto possa ser qualquer subtipo de Jogo
,
só os métodos acessíveis na classe Jogo
podem ser invocados sobre esses objetos
Jogo
;aquilo que se espera obter na invocação de métodos sobre esses objetos, em termos de contratos, deve ser o que está definido na classe Jogo
; tomemos o exemplo do método vencedores
:
se a pré-condição definida para o método na classe Jogo
for satisfeita na altura da invocação, então o método deve poder ser invocado sem problemas, mesmo que a versão executada seja outra, por via de redefinição:
após a invocação do método, a pós-condição definida para ele na classe Jogo
tem que ser garantida, mesmo que a versão executada seja outra, por via de redefinição:
Ainda usando o exemplo do método vencedores
, relembremos a linha de comentário que define a sua pré-condição na classe Jogo
:
* @requires this.quantosEmJogo() > 0 && this.terminou()
Na redefinição deste método na classe JogoComObjetivo
, a pré-condição não poderá ser mais restritiva (mais forte). Deverá ser igual ou menos restritiva (mais fraca):
@requires this.quantosEmJogo() > 0
estaria correto, pois é menos restritiva, mais fraca;@requires this.quantosEmJogo() > 2 && this.terminou()
estaria incorreto pois é mais exigente, mais forte;@requires this.quantosEmJogo() > 0 && this.terminou() && this.pontuacaoObjetivo() > this.maiorPontuacao()
também estaria incorreto pois é mais exigente.
Vamos agora ver o exemplo do método void registarPontosJogada(String nome, int pontos)
. Embora não tenhamos apresentado pós-condição para este método na classe Jogo
, ela poderia ser:
xxxxxxxxxx
* @ensures this.pontuacao(nome) == \old this.pontuacao(nome) + pontos &&
pontos > \old this.maximoNumaJogada(nome)
implies
this.maximoNumaJogada(nome) == pontos
Na redefinição deste método na classe JogNumeroExatoJogadas
, a pós-condição deverá garantir esta condição ou outra mais forte:
A seguinte pós-condição estaria correta pois é mais forte:
xxxxxxxxxx
* @ensures this.pontuacao(nome) == \old this.pontuacao(nome) + pontos &&
pontos > \old this.maximoNumaJogada(nome)
implies
this.maximoNumaJogada(nome) == pontos
&&
this.jogadasJahFeitas() == \old this.jogadasJahFeitas() + 1 &&
this.jogadasJahFeitas() == this.numeroJogadasAFazer()
implies
this.terminou()
A seginte pós-condição estaria incorreta pois assegura menos, é mais fraca:
@ensures this.pontuacao(nome) == \old this.pontuacao(nome) + pontos
;
No geral,
para duas classes
A
eB
, em queB
é subclasse deA
, temos que, para todo o métodom
acessível aos clientes deA
:
m
está também acessível emB
– pelo mecanismo de herança;- a pré-condição de
m
emB
não pode ser mais forte do que a declarada emA
;- a pós-condição de
m
emB
não pode ser mais fraca do que a declarada emA
.Ou seja,
B
não pode exigir mais nem prometer menos!
Isto leva-nos ao princípio conhecido por Liskov substitution principle:
Só fazendo com que a subclasse honre os contratos da superclasse conseguimos garantir que:
- o raciocínio feito em termos da superclasse é valido para as subclasses e, por isso,
- um objeto com tipo
S
, subtipo deT
, pode ser usado em qualquer sítio em que é esperado um objeto com o tipoT
(sendo o comportamento consistente com o especificado porT
).
Anterior: 15.4. Invocação indireta de métodos redefinidos
Seguinte: 15.6. Tipos genéricos e sub-tipos