CodeContracts para poner contratos a LINQ

octubre 12, 2009
By

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.

image

Figura 1. Mensaje por violación de pos-condición

image

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.

Tags: ,

Deja un comentario

Tu dirección de correo electrónico no será publicada. Los campos necesarios están marcados *

*

Acerca del autor...

Miguel Katrib

Miguel Katrib
Miguel Katrib is Dr. and Full Professor of the Programming Department at the Faculty of Mathematics and Computer Science of the University of Havana and director of the Master in Science program in ...Leer completo