|
|
@@ -35,8 +35,8 @@
|
|
|
\input{tipos/atleta.tex}
|
|
|
|
|
|
\begin{problema}{especialidad}{a: Atleta}{Deporte}
|
|
|
- \asegura{result \in deportes(a)}
|
|
|
- \asegura{capacidad(a,result)==maximoLista(listarCapacidades(a))}
|
|
|
+ \asegura{res \in deportes(a)}
|
|
|
+ \asegura{capacidad(a,res)==maximoLista(listarCapacidades(a))}
|
|
|
\aux{listarCapacidades}{a:Atleta}{[\ent]}{[capacidad(a,x) | x \leftarrow deportes(a) ]}
|
|
|
\aux{maximoLista}{ls:[\ent]}{\ent}{[x|x\leftarrow ls, (\forall y \leftarrow ls) x \geq y][0]}
|
|
|
\end{problema}
|
|
|
@@ -45,7 +45,14 @@
|
|
|
\requiere{c \geq 0 \wedge c \leq 100}
|
|
|
\requiere{d \notin deportes(a)}
|
|
|
\modifica{a}
|
|
|
- \asegura{mismos(deportes(a),deportes(pre(a)))}
|
|
|
+ \asegura{nombre(a)==nombre(pre(a))}
|
|
|
+ \asegura{sexo(a) == sexo(pre(a))}
|
|
|
+ \asegura{añoNacimiento(a)==añoNacimiento(pre(a))}
|
|
|
+ \asegura{nacionalidad(a)==nacionalidad(pre(a))}
|
|
|
+ \asegura{ciaNumber(a)==ciaNumber(pre(a))}
|
|
|
+ \asegura{(\forall d' \leftarrow deportes(pre(a)))capacidad(a,d')==capacidad(pre(a),d')}
|
|
|
+
|
|
|
+ \asegura{mismos(deportes(a),d:deportes(pre(a)))}
|
|
|
\asegura{ordenada(deportes(a))}
|
|
|
\asegura{capacidad(a,d)==c}
|
|
|
\end{problema}
|
|
|
@@ -82,7 +89,7 @@
|
|
|
|
|
|
\begin{problema}{gananLosMasCapaces}{c: Competencia}{\bool}
|
|
|
\requiere{finalizada(c)}
|
|
|
- \asegura{result==(\forall x \leftarrow[0..|ranking(c)|-2]) \newline
|
|
|
+ \asegura{res==(\forall x \leftarrow[0..|ranking(c)|-2]) \newline
|
|
|
capacidad(ranking(c)[x],prm(categoria(c))) \geq capacidad(ranking(c)[x+1],prm(categoria(c)))}
|
|
|
\end{problema}
|
|
|
|
|
|
@@ -104,7 +111,7 @@
|
|
|
\input{tipos/jjoo.tex}
|
|
|
|
|
|
\begin{problema}{dePaseo}{j: JJOO}{[Atleta]}
|
|
|
- \asegura{result==noParticiparon(j)}
|
|
|
+ \asegura{res==noParticiparon(j)}
|
|
|
\aux{noParticiparon}{j: JJOO}{[Atleta]}{[x | x \leftarrow atletas(j), \neg en(x, participaronConRepes(j))]}
|
|
|
\aux{participaronConRepes}{j: JJOO}{[Atleta]}{[atl | dia \leftarrow [1..cantDias(j)], comp \leftarrow cronograma(j, dia), atl \leftarrow atletas(j), en(atl, participantes(comp))]}
|
|
|
|
|
|
@@ -119,10 +126,10 @@
|
|
|
|
|
|
|
|
|
\begin{problema}{losMasFracasados}{j: JJOO, p: Pais}{[Atleta]}
|
|
|
- %\\asegura{(\forall x \rightarrow [ciaNumber(ranking(comp)[0]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[1]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[2]) \neq ciaNumber(atl) | atl \rightarrow result, comp \rightarrow todasLasCompetencias(j), finalizada(comp)]) x}
|
|
|
- %\\asegura{(\forAll x \rightarrow [ciaNumber(ranking(comp)[0]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[1]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[2]) \neq ciaNumber(atl) | atl \rightarrow result, comp \rightarrow todasLasCompetencias(j), finalizada(comp)]) x}
|
|
|
- %\\asegura{(\forAll x \rightarrow result) nacionalidad(x) == p}
|
|
|
- %\\asegura{(\forAll i \rightarrow [0..|result|-2]) competenciasEnLasQueParticipo(j, result[i]) \geq competenciasEnLasQueParticipo(j, result[i+1])}
|
|
|
+ %\\asegura{(\forall x \rightarrow [ciaNumber(ranking(comp)[0]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[1]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[2]) \neq ciaNumber(atl) | atl \rightarrow res, comp \rightarrow todasLasCompetencias(j), finalizada(comp)]) x}
|
|
|
+ %\\asegura{(\forAll x \rightarrow [ciaNumber(ranking(comp)[0]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[1]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[2]) \neq ciaNumber(atl) | atl \rightarrow res, comp \rightarrow todasLasCompetencias(j), finalizada(comp)]) x}
|
|
|
+ %\\asegura{(\forAll x \rightarrow res) nacionalidad(x) == p}
|
|
|
+ %\\asegura{(\forAll i \rightarrow [0..|res|-2]) competenciasEnLasQueParticipo(j, res[i]) \geq competenciasEnLasQueParticipo(j, res[i+1])}
|
|
|
%\\aux{competenciasEnLasQueParticipo}{j: JJOO, a: Atleta}{\ent}{\longitud{[z | z \leftarrow todasLasCompetencias(j), en(a, participantes(z))]}}
|
|
|
\end{problema}
|
|
|
|
