Slides TD Parcial1-21-30

Vista previa del material en texto

Entendiendo cuantificadores: ∃
I (∃i : int) (0 ≤ i < |v | ∧ v [i ] = 2)
I Significa que alguna de las sigs. fórmulas tiene que ser Verdadera:
−∞
...
(0 ≤ −2 < |v | ∧ v [−2] = 2)
(0 ≤ −1 < |v | ∧ v [−1] = 2)
(0 ≤ 0 < |v | ∧ v [0] = 2)
(0 ≤ 1 < |v | ∧ v [1] = 2)
...
(0 ≤ |v | − 2 < |v | ∧ v [|v | − 2] = 2)
(0 ≤ |v | − 1 < |v | ∧ v [|v | − 1] = 2)
(0 ≤ |v | < |v | ∧ v [|v |] = 2)
(0 ≤ |v |+ 1 < |v | ∧ v [|v |+ 1] = 2)
...
∞ 4
Entendiendo cuantificadores: ∃
I (∃i : int) (0 ≤ i < |v | ∧ v [i ] = 2)
I Significa que alguna de las sigs. fórmulas tiene que ser Verdadera:
−∞
...
Falso
Falso
v [0] = 2
v [1] = 2
...
v [|v | − 2] = 2
v [|v | − 1] = 2
Falso
Falso
...
∞ 4
El caso de la doble implicación
I Nuestro lenguaje de especificación no tiene el símbolo de doble
implicación ⇐⇒ .
I (∀x , y : int) 10 = y ∗ x ⇐⇒ 10/x = y
I ¿Qué pasa en el caso x = 0? ¿Cómo manejamos la indefinición del
lado derecho del ⇐⇒ ?
I Recordar: en lógica trivaluada importa el orden de la fórmula en caso
de indefiniciones.
I ¿Cuál de las siguientes formulas es equivalente a P ⇐⇒ Q?
I (P =⇒ Q) ∧ (Q =⇒ P)
I (Q =⇒ P) ∧ (P =⇒ Q)
I En lugar de elegir, no tenemos semántica trivaluada para ⇐⇒ .
I Ustedes deben razonar para cada caso, cómo manejar las
indefiniciones y escribir la fórmula con =⇒ .
I En caso de que ni P ni Q se indefinan pueden usar ⇐⇒ como
abuso de notación para simplificar la escritura.
5
Razonando sobre especificaciones
¿Cumplen los programas P1 y P2 el contrato C?
Contrato C :
float maximo(float a, float b)
Pre: Verdadero
Post: (res = a ∨ res = b) ∧ (res ≥ a ∧ res ≥ b)
Programa P1:
1 float maximo(float a, float b){
2 return a + b;
3 }
Programa P2:
1 float maximo(float a, float b){
2 float res = a;
3 if(b > a){
4 res = b;
5 }
6 return res;
7 } 6
Razonando sobre especificaciones
Programas:
P2
P3
P4
P5P6
P7
P8 P9
P10 P1
Contrato:
C
8
Sub y sobre especificación
Programas:
P2 P5
P7
P9
Especificación
correcta
9
Sub y sobre especificación
Programas:
P2 P5
P7
P9
Sobre
especificación
Sub
especificación
P8
P1
9
Sub y sobre especificación
Son problemas que consisten en dar una especificación que no se ajusta
correctamente al problema que queremos describir.
Sub-especificamos cuando
(a) damos más condiciones sobre las entradas (Pre) que las que tendría
sentido para nuestro problema, dejando afuera entradas válidas;
(b) damos muy pocas condiciones sobre las salidas (Post), aceptando
salidas erróneas para el problema
Aceptamos programas incorrectos como válidos
Sobre-especificamos cuando
(a) damos menos condiciones en (Pre) que las necesarias;
(b) damos más condiciones sobre las salidas (Post) que las necesarias;
Rechazamos programas correctos como inválidos
10
Sub y sobre especificación: ejemplos
Dados dos números a y b, calcular su producto.
float producto(float a, float b)
Pre: a > 0 ∧ b > 0
Post: res = a ∗ b
Subespecificación; restringe innecesariamente a y b a que sean positivos.
Acepta programas que sólo puedan multiplicar números positivos.
Dado un entero k y un vector de enteros S que contiene a k , dar la
posición de la primera aparición de k en S .
int buscar_primera(int k, vector<int> S)
Pre: (∃j : int) 0 ≤ j < |S | ∧ S [j ] = k
Post: 0 ≤ res < |S | ∧ S [res] = k
Subespecificación; no garantiza que la posición devuelta sea la primera
aparición. Acepta programas que devuelvan otras apariciones.
11
Sub/sobre especificación: ejemplos (II)
Dado un entero k y un vector de enteros S que contiene a k dar la
posición de alguna aparición de k en S .
int buscar_alguna(int k, vector<int> S)
Pre: (∃j : int) 0 ≤ j < |S | ∧ S [j ] = k
Post: 0 ≤ res < |S |∧S [res] = k∧(∀j : int)0 ≤ j < res =⇒ S [j ] 6= k
Sobreespecificación; rechaza programas que devuelvan una aparición que
no sea la primera.
Dados dos vectores de caracteres s y t, indicar si s aparece como
subcadena de t.
bool es_subcadena(vector<char> s, vector<char> t)
Pre: |s| ≤ |t|
Post: res = true ⇐⇒ (∀i : int) 0 ≤ i < |s| =⇒ s[i ] = t[i ]
Sobreespecificación; está restringiendo a que s sea prefijo de t
Subespecificación; no es necesario restringir las longitudes de s y t. 12