[No Resuelto] Parcial de Especificación - septiembre 2011

Subo el parcial que entregaron el lunes en clase a ver si alguien quiere compartir sus respuestas, revisar las que yo vaya poniendo.

Ej. 1 a)
\(invariante \; losHorariosDeUnMismoEmpleadoNoSeSolapan \; :\)
\((\forall e \leftarrow empleados(b) ) \; sinRepetidos( [ \; x \; \vert \; h \leftarrow horarios(b,e), \; x \leftarrow [prm(h) .. prm(h)+sgd(h)-1] ] )\)

Ej. 1 b)

\(invariante \; siempreUnoDeGuardia :\)
\((\forall n \leftarrow [0..23]) \; n \in [ \; x \; \vert \; e \leftarrow empleados(b), \; h \leftarrow horarios(b,e), \; x \leftarrow [prm(h)..prm(h)+sgd(h)-1] \; ]\)

Ej 1. c)

\(invariante \; aReglamento :\)
\((\forall e \leftarrow empleados(b)) \; long(\; [ \; x \; \vert \; h \leftarrow horarios(b,e), \, x \leftarrow [prm(h)..prm(h)+sgd(h)-1] \; ) \leq convenioHoras(sindicato(e)) ;\)