<details>
<summary>*Idiom* para definir aserciones finales</summary>
A veces hace falta guardar datos antes de hacer un cómputo, para poder luego comprobar una condición cuando el cómputo se haya completado.
Ejemplo de cómo hacerlo con una _inner class_ que guarda el estado de variables:
```java
void foo(int[] array) {
// Manipulate array
...
// At this point, array will contain exactly the ints that it did
// prior to manipulation, in the same order.
}
void foo(final int[] array) {
class DataCopy {
private int[] arrayCopy;
DataCopy() { arrayCopy = (int[])(array.clone()); }
boolean isConsistent() { return Arrays.equals(array, arrayCopy); }
}
DataCopy copy = null;
// Always succeeds; has side effect of saving a copy of array
assert (copy = new DataCopy()) != null;
... // Manipulate array
assert copy.isConsistent();
}
```
</details>
- Eiffel no permite que se pueda cambiar el valor de un parámetro (es inmutable)
---
### Ejemplo: Raíz cuadrada en Eiffel
```eiffel
sqrt: DOUBLE is
-- Square root routine
require
sqrt_arg_must_be_positive: Current >= 0;
--- ...
--- calculate square root here
--- ...
ensure
((Result*Result) - Current).abs <= epsilon*Current.abs;
-- Result should be within error tolerance
end;
```
---
Si el usuario introduce un número negativo en la consola, es responsabilidad del código que llama a `sqrt` que dicho valor no se pase nunca a `sqrt`. Opciones:
- Terminar
- Emitir una advertencia y leer otro número
- Pasar el número a complejo (ponerlo en positivo y añadir una _i_)
Si se llega a pasar un número negativo, Eiffel imprime el error `sqrt_arg_must_be_positive` en tiempo de ejecución y una traza de la pila.
En otros lenguajes, como Java, se devolvería un `NaN`.
---
### Ejemplo: Cuenta Bancaria
#### Cuenta Bancaria sin contratos
```eiffel
class ACCOUNT
feature
balance: INTEGER
owner: PERSON
minimum_balance: INTEGER is 1000
open (who: PERSON) is
-- Assign the account to owner who.
do
owner := who
end
deposit (sum: INTEGER) is
-- Deposit sum into the account.
do
add (sum)
end
```
---
```eiffel
withdraw (sum: INTEGER) is
-- Withdraw sum from the account.
do
add (-sum)
end
may_withdraw (sum: INTEGER): BOOLEAN is
-- Is there enough money to withdraw sum?
do
Result := (balance >= sum + minimum_balance)
end
```
---
```eiffel
feature {NONE}
add (sum: INTEGER) is
-- Add sum to the balance.
do
balance := balance + sum
end
end -- class ACCOUNT
```
- `feature` son las operaciones de la clase
- `feature { NONE }` son privados
- `make` para definir el constructor
---
#### Cuenta Bancaria con contratos
```eiffel
class ACCOUNT
create
make
feature
-- ... Attributes as before:
balance, minimum_balance, owner, open ...
deposit (sum: INTEGER) is
-- Deposit sum into the account.
require
sum >= 0
do
add (sum)
ensure
balance = old balance + sum
end
```
---
```eiffel
withdraw (sum: INTEGER) is
-- Withdraw sum from the account.
require
sum >= 0
sum <= balance - minimum_balance
do
add (-sum)
ensure
balance = old balance - sum
end
may_withdraw ... -- As before
```
---
```eiffel
feature {NONE}
add ... -- As before
make (initial: INTEGER) is
-- Initialize account with initial balance.
require
initial >= minimum_balance
do
balance := initial
end
invariant
balance >= minimum_balance
end -- class ACCOUNT
```
---
__Forma corta__ del contrato:
```eiffel
class interface ACCOUNT
create
make
feature
balance: INTEGER
...
deposit (sum: INTEGER) is
-- Deposit sum into the account.
require
sum >= 0
ensure
balance = old balance + sum
withdraw (sum: INTEGER) is
-- Withdraw sum from the account.
require
sum >= 0
sum <= balance - minimum_balance
ensure
balance = old balance - sum
may_withdraw (...): BOOLEAN is ...
end -- class ACCOUNT
```
### Precondiciones con aserciones
#### Método público
```java
/**
* Sets the refresh rate.
*
* @param rate refresh rate, in frames per second.
* @throws IllegalArgumentException if rate <= 0 or
* rate > MAX_REFRESH_RATE.
*/
public void setRefreshRate(int rate) {
// Enforce specified precondition in public method
if (rate <= 0 || rate > MAX_REFRESH_RATE)
throw new IllegalArgumentException("Illegal rate: " + rate);
setRefreshInterval(1000/rate);
}
```
- El método garantiza que siempre se harán chequeos de los argumentos, independientemente de si las aserciones están o no activadas
- Añadir un assert para la precondición no es apropiado en este caso
#### Método no público
```java
/**
* Sets the refresh interval (must correspond to a legal frame rate).
*
* @param interval refresh interval in milliseconds.
*/
private void setRefreshInterval(int interval) {
// Confirm adherence to precondition in nonpublic method
assert interval > 0 && interval <= 1000/MAX_REFRESH_RATE : interval;
... // Set the refresh interval
}
```
- La aserción indica una precondición que debe ser cierta sin importar lo que el cliente haga con la clase
- La aserción puede indicar un bug en la biblioteca
### Postcondiciones con aserciones
- Pueden usarse en métodos públicos y no públicos
```java
/**
* Returns a BigInteger whose value is (1/this mod m).
*
* @param m the modulus.
* @return 1/this mod m.
* @throws ArithmeticException m <= 0, or this BigInteger
* has no multiplicative inverse mod m
* (this BigInteger is not relatively prime to m).
*/
public BigInteger modInverse(BigInteger m) {
if (m.signum <= 0)
throw new ArithmeticException("Modulus not positive: " + m);
... // Do the computation
assert this.multiply(result).mod(m).equals(ONE) : this;
return result;
}
```
### Cuestiones de Diseño
(LSP) Inheritance and polymorphism are the cornerstones of object-oriented languages and an area where contracts can really shine. Suppose you are using inheritance to create an "is-a-kind-of" relationship, where one class "is-a-kind-of" another class. You probably want to adhere to the Liskov Substitution Principle
Without a contract, all the compiler can do is ensure that a subclass conforms to a particular method signature. But if we put a base class contract in place, we can now ensure that any future subclass can't alter the meanings of our methods. For instance, you might want to establish a contract for setFont such as the following, which ensures that the font you set is the font you get:
/**
* @pre f != null
* @post getFont() == f
*/
public void setFont(final Font f) {
// ...