Miguel Katrib
En Code Contracts hay la posibilidad de usar, dentro de los contratos, el cuantificador universal Contract.ForAll y el cuantificador existencial Contract.Exists.
Contract.ForAll tiene dos argumentos, el primero es una colección expresada por el tipo genérico IEnumerable<T> y el segundo es un predicado expresado por el tipo Predicate<T>, donde un predicado es un método de un argumento que retorna un bool. Retorna true si todos los elementos de la colección evalúan true en dicho predicado y retorna false en caso contrario.
Contract.Exists tiene los mismos parámetros que el Contract.ForAll. En este caso el predicado se aplica a cada elemento de la colección, si en uno de ellos evalúa true el resultado será true y si todos evalúan false el resultado será false.
Note, por ejemplo que el resultado de
Contract.Ensures(Contrat.ForAll(colección, predicado);
es el mismo que el de
Contract.Ensures(colección.All(predicado));
Del mismo modo las dos construcciones siguientes dan igual resultado
Contract.Ensures(Contrat.Exists(colección, predicado);
Contract.Ensures(colección.Any(predicado));
static class ContractedLINQMethods { public static IEnumerable<IGrouping<K, T>> GroupBy<T, K>(this IEnumerable<T> source, Func<T, K> selector) { Contract.Ensures(Contract.ForAll( Contract.Result<IEnumerable<IGrouping<K, T>>>(), x => x.All(y => selector(y).Equals(x.Key) && source.Contains(y))), "Todos los elementos de un grupo tienen la misma llave del grupo y" + "están en la colección original"); Contract.Ensures(Contract.Result<IEnumerable<IGrouping<K, T>>>(). Select(x => x.Count()).Sum() == source.Count(), "La suma de las cantidades de cada grupo es igual a la cantidad de la" + "colección original"); //...otras pos-condiciones para GroupBy return Enumerable.GroupBy(source, selector); } //...otros métodos de LINQ }
Listado 1. Poniendo contratos a métodos de linq
La inclusión de poder usar cuantificadores en los contratos aumenta la capacidad expresiva de los mismos. Muchos tipos relacionados con colecciones, en especial la “maquinaria” de LINQ, se verían enriquecidos en su definición si incluyesen ahora contratos con cuantificadores.
En el Listado 1 se muestra cómo podrían añadírsele dos pos-condiciones a un método como GroupBy. Si por ejemplo cambiamos la sentencia return Enumerable.GroupBy(source, selector); por la instrucción return Enumerable.GroupBy(source, selector).Skip(1); (note que estamos forzando que el resultado sea incorrecto al quitar uno de los grupos) entonces violaríamos la segunda pos-condición. En este caso, si el chequeo de las pos-condiciones está activado, la ejecución de un código que haga GroupBy provocaría violación de la segunda pos-condición
static class ContractedLINQMethods { public static IEnumerable<IGrouping<K, T>> GroupBy<T, K>(this IEnumerable<T> source, Func<T, K> selector) { //... Contract.Ensures(Contract.ForAll(source, (x =>Contract.Result<IEnumerable<IGrouping<K, T>>>() .Any(y => y.Contains(x)))), "Todo elemento de la colección original está en algún grupo"); //... } //... }
Listado 2. Añadiendo una nueva pos-condicion a GroupBy
produciendo el mensaje que se muestra en la Figura 1.
Sin embargo, si ponemos una pos condición como la del listado 2, entonces el intento de ejecución reportaría un extraño error como el que se muestra en la Figura 2. Este error se produce incluso antes ejecutar el método ContractedLINQMethods.GroupBy! No conocemos las causas de este bug, todo parece indicar que se debe al intento de usar Contract.Result dentro de una expresión lambda que es a su vez argumento de una iteración. Esperamos que esto esté resuelto en la versión final de VS2010.
Figura 1. Mensaje por violación de pos-condición
Figura 2. Bug en la carga Mensaje por violación de pos-condición
Esto es solo una muestra, lo invitamos a ponerle contratos a todos los métodos de LINQ.
