Post on 27-Sep-2020
Programación 2Lección 2: Especificación formal de
algoritmos que trabajan conestructuras de datos indexadas
Algunos tipos de datos que utilizaremosstruct Fecha{
int dia, mes, anyo; // dia,mes,anyo};struct Nif{
int dni; // numero del DNIchar letra; // letra asociada al DNI
};struct Persona{
Nif nif; // NIF de la personaFecha nacimiento; // su fecha de nacimientobool estaCasada; // casado (T)/soltero (F)bool esHombre; // hombre (T)/mujer (F)
};
Estructura de datos indexadaEspecificaciones y número de componentes
// Pre: ????// Post: sumaComp(a,p,f) =
∑α ∈ [p, f ].a[α]
int sumaComp(const int a[], const int p,const int f);
int v[10]; // reserva memoria para 10 intdouble m[3][4]; // reserva mem. para 12 double...int s = sumaComp(v,0,20);// analizar su comportamiento
// Pre: 0 ≤ p ≤ f ∧ f < #a// Post: sumaComp(a,p,f) =
∑α ∈ [p, f ].a[α]
int sumaComp(const int a[], const int p,const int f);
int v[10]; // reserva memoria para 10 intdouble m[3][4]; // reserva mem. para 12 double
Donde (solo en predicados y aserciones, no en código C++):
I #a: número de componentes del vector a
I #v: número de componentes del vector v
I #m(1) o #m: número de filas de la matriz m
I #m(2): número de columnas de la matriz m
Especificación de funciones de recorrido
// Pre: 0 ≤ n ≤ #v// Post: cuentaPares(v,n) =// Num α ∈ [0, n − 1].v[α] %2 = 0
int cuentaPares(const int v[],const int n);
// Pre: 0 ≤ p ∧ f < #v// Post: anonima(v,p,f,minimo,maximo) =// Num α ∈ [p, f ].minimo ≤ v[α] ≤ maximo
int anonima(const double v[],const int p, const int f,const double minimo,const double maximo);
// Pre: 1 < n ≤ #TNif// Post: anonima(TNif,n) = NifMasBajo ∧// ∃α ∈ [0, n − 1].TNif [α] = NifMasBajo ∧// ∀α ∈ [0, n − 1].TNif [α].dni ≥ NifMasBajo.dni
Nif anonima(const Nif TNif[], const int n);
// Pre: 0 ≤ n ≤ #TP// Post: anonima(TP,n,m) =// Num α ∈ [0, n − 1].TP[α].nacimiento.mes = m
int anonima(const Persona TP[], const int nconst int m);
Especificación de funciones de búsqueda
// Pre: 0 ≤ n ≤ #v// Post: anonima(v,n) =// ∀α ∈ [0, n − 2].v[α] ≤ v[α + 1]
bool anonima(const int v[], const int n);
// Pre: 0 ≤ n ≤ #TP// Post: anonima(TP,n) =// ∀α ∈ [0, n − 2].TP[α].nif .dni ≤ TP[α + 1].nif .dni
bool anonima(const Persona TP[], const int n);
// Pre: 0 ≤ p ∧ f < #v// Post: anonima(v,p,f,dato) =// ∃α ∈ [p, f ].v[α] = dato
bool anonima(const int v[], const int pconst int f, const int dato);
// Pre: 0 ≤ p ∧ f < #v ∧// ∀α ∈ [p, f − 1].v[α] ≤ v[α + 1]// Post: anonima(v,p,f,dato) =// ∃α ∈ [p, f ].v[α] = dato
bool anonima(const int v[], const int pconst int f, const int dato);
// Pre: n ≤ #TP ∧// ∃α ∈ [0, n − 1].¬TP[α].estaCasada// Post: anonima(TP,n) = S ∧ ¬S .estaCasada∧// ∃α ∈ [0, n − 1].TP[α] = S
Persona anonima(const Persona TP[],const int n);
// Pre: n ≤ #TP ∧// ∃α ∈ [0, n − 1].TP[α].esHombre// Post: anonima(TP,n) = INDICE ∧// INDICE ≥ 0 ∧ INDICE ≤ n − 1 ∧// TP[INDICE ].esHombre ∧// ∀α ∈ [0, INDICE − 1].¬TP[α].esHombre
int anonima(const Persona TP[], const int n);
Especificación de algoritmos decomparación de dos vectores o tablas
// Pre: 0 ≤ n ≤ #v1 ∧ n ≤ #v2// Post: anonima(v1,v2,n) =// ∀α ∈ [0, n − 1].v1[α] = v2[α]
bool anonima(const int v1[],const int v2[],const int n);
// Pre: 0 ≤ n ≤ #v1 ∧ n ≤ #v2// Post: anonima(v1,v2,n) =// ∀α ∈ [0, n − 1].∃β ∈ [0, n − 1].v2[β] = v1[α] ∧// ∀α ∈ [0, n − 1].∃β ∈ [0, n − 1].v1[β] = v2[α]
bool anonima(const int v1[],const int v2[],const int n);
// Pre: 0 ≤ n ≤ #v1 ∧ n ≤ #v2// Post: anonima(v1,v2,n) =// ∀α ∈ [0, n − 1].// (Num β ∈ [0, n − 1].v1[β] = v1[α]) =// (Num β ∈ [0, n − 1].v2[β] = v1[α])
bool anonima(const int v1[],const int v2[],const int n);
Especificación de algoritmos quemodifican un vector o una tabla
// Pre: 0 ≤ n ≤ #v ∧ v = V0// Post: ∀α ∈ [0, n − 1].// (V0[α] < 0.0→ v[α] = 0.0) ∧// (V0[α] ≥ 0.0→ v[α] = V0[α])
void anonima(double v[], const int n);
// Pre: 0 ≤ n ≤ #v ∧ v = V0// Post: ∀α ∈ [0, n − 1].// (V0[α] = x → v[α] = y) ∧// (V0[α] 6= x → v[α] = V0[α])
void anonima(int v[], const int n,const int x, const int y);
// Pre: 0 ≤ n ≤ #TP ∧ TP = TP0// Post: ∀α ∈ [0, n − 1].// (Num β ∈ [0, n − 1].TP[α] = TP[β]) =// (Num β ∈ [0, n − 1].TP[α] = TP0[β]) ∧// ∀α ∈ [0, n − 1].// (¬TP[α].estaCasada →// (∀β ∈ [0, α].¬TP[β].estaCasada)) ∧// (TP[α].estaCasada →// (∀β ∈ [α, n − 1].TP[β].estaCasada))
void anonima(Persona TP[], const int n);
// Pre: 0 ≤ n ≤ #TP ∧ TP = TP0// Post: sonPermutacion(TP,TP0, 0, n − 1) ∧// ∀α ∈ [0, n − 1].// (¬TP[α].estaCasada →// (∀β ∈ [0, α].¬TP[β].estaCasada)) ∧// (TP[α].estaCasada →// (∀β ∈ [α, n − 1].TP[β].estaCasada))
void anonima(Persona TP[], const int n);
Donde://sonPermutacion(Ta,Tb, p, f ) ≡// ∀α ∈ [p, f ].// (Num β ∈ [p, f ].Ta[α] = Ta[β]) =// (Num β ∈ [p, f ].Ta[α] = Tb[β])
// Pre: 0 ≤ n ≤ #v ∧ v = V0// Post: sonPermutacion(v,V0, 0, n − 1) ∧// ordenado(v, 0, n − 1)
void anonima(int v[], const int n);
Donde://sonPermutacion(Ta,Tb, p, f ) ≡// ∀α ∈ [p, f ].// (Num β ∈ [p, f ].Ta[α] = Ta[β]) =// (Num β ∈ [p, f ].Ta[α] = Tb[β])//ordenado(T , p, f ) ≡// ∀α ∈ [p, f − 1].T [α] ≤ T [α + 1]