El estado sombrío de las bibliotecas de pruebas basadas en propiedades

 (stevana.github.io)
1 puntos por GN⁺ 2024-07-06 | 1 comentarios | Compartir por WhatsApp
  • Las pruebas basadas en propiedades se extendieron a muchos lenguajes después de QuickCheck, pero a julio de 2024 muchas bibliotecas aún no ofrecen de forma suficiente las pruebas basadas en estado y las pruebas paralelas, que ya habían quedado sistematizadas en 2009
  • La brecha central está en la capacidad de verificar cambios de estado secuenciales con un modelo de máquina de estados y reutilizar ese mismo modelo para una comprobación de linealizabilidad (linearisability) que permita encontrar race conditions en ejecuciones paralelas
  • En muchos de los proyectos analizados, las pruebas basadas en estado no existen o son experimentales, y las pruebas paralelas son aún más raras; en FsCheck, Gopter, RapidCheck, SwiftCheck, jsverify y otros siguen abiertos issues relacionados desde hace años
  • Una implementación en Haskell de unas 400 líneas reproduce las pruebas basadas en propiedades con estado y paralelas, y en lugar de una especificación tradicional con máquina de estados usa como modelo una implementación de referencia basada en fake, más familiar para los programadores
  • Un fake probado por contrato puede reutilizarse no solo para validar un componente individual, sino también para pruebas de integración rápidas y deterministas, inyectándolo en lugar de dependencias reales

La brecha de funcionalidades que se abrió después de QuickCheck

  • Las pruebas basadas en propiedades se difundieron en comunidades de varios lenguajes de programación bajo la consigna de “no escribas tests, genéralos”
  • La página de Wikipedia de QuickCheck, la biblioteca original de Haskell, enumera 57 reimplementaciones en otros lenguajes
  • El primer paper de QuickCheck, QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs, se presentó en ICFP 2000, y el código fuente completo de la primera implementación ocupaba unas 300 líneas en el apéndice del paper
  • El QuickCheck inicial solo podía probar funciones puras, y en 2002 Testing monadic code with QuickCheck sentó las bases para tratar código con efectos como estado mutable, file I/O y networking

La aparición de las pruebas basadas en estado y paralelas

  • Quviq AB fue fundada en 2006 por John Hughes y Thomas Arts, y las pruebas de proyectos Erlang de Ericsson estuvieron entre sus primeros casos de uso
  • Erlang no es un lenguaje funcional puro y la concurrencia es común, por lo que el QuickCheck monádico existente no era lo suficientemente cómodo de usar
  • El QuickCheck de Erlang de código cerrado de Quviq incorporó dos funcionalidades que luego faltaron en varias implementaciones open source
    • Pruebas basadas en propiedades secuenciales y con estado usando un modelo de máquina de estados
    • Pruebas paralelas que reutilizan el mismo modelo de máquina de estados secuencial para detectar race conditions
  • Las pruebas basadas en estado aparecieron en su forma actual en QuickCheck testing for fun and profit (2007)
  • Las pruebas paralelas se trataron en detalle en Finding Race Conditions in Erlang with QuickCheck and PULSE (ICFP 2009), tomando como técnica central Linearizability: a correctness condition for concurrent objects (1990), de Herlihy y Wing
  • El código de biblioteca de Quviq QuickCheck no se compartió en los papers; lo que se publicó fue la API y ejemplos de tests que usaban esa API

Resultados del relevamiento de bibliotecas en 2024

  • El estado del arte actual es el stateful testing basado en modelos de máquina de estados y el parallel testing que combina linearisability con el mismo modelo secuencial
  • El relevamiento se hizo a julio de 2024 leyendo documentación, issue trackers y parte del código fuente
  • Muchas bibliotecas no ofrecen pruebas basadas en estado o las ofrecen de forma limitada
    • QuickCheck (Haskell) tiene abierto desde 2016 un issue para agregar pruebas basadas en estado
    • SwiftCheck también tiene abierto desde 2016 un issue para agregar pruebas basadas en estado
    • jsverify mantiene desde 2015 un issue para agregar pruebas basadas en estado
    • proptest (Rust) requiere consultar por separado proptest-state-machine
  • El soporte para pruebas paralelas es aún más raro
    • En el README de Gopter dice “No parallel commands … yet?” y hay un issue de 2017
    • FsCheck tiene abierto desde 2016 un issue para agregar parallel support
    • RapidCheck tiene abierto desde 2015 un issue para agregar parallel support
    • propcheck tiene desde 2020 un issue para agregar parallel testing
  • Como ejemplos open source que soportan ambas funcionalidades se mencionan PropEr, Hedgehog, qcheck-stm, quickcheck-state-machine y stateful-check
  • Hay casos con limitaciones incluso cuando existe funcionalidad paralela
    • En comentarios del código fuente de QuickTheories se indica que, en sus pruebas paralelas, la cantidad de end states posibles crece rápidamente con el número de comandos, por lo que normalmente hay que limitar la command list a 10 elementos o menos
    • Los ejemplos de LevelDB y Redis de ScalaCheck se presentan como ejemplos secuenciales con threadCount = 1
    • El soporte de race conditions de fast-check, a diferencia de las pruebas paralelas de Quviq QuickCheck, no parece reutilizar un modelo de máquina de estados secuencial ni usar linearisability
  • No se observan ejemplos claros en los que las pruebas paralelas se hayan agregado más tarde; si no se contemplan en el diseño inicial de la API, puede ser necesario un rediseño considerable

Por qué la difusión de estas funcionalidades fue lenta

  • John Hughes propuso tres razones
    • Las pruebas basadas en estado y paralelas no son tan útiles como las pruebas de funciones puras
    • Escribir modelos de máquina de estados requiere una forma de pensar distinta a la de los tests comunes y exige capacitación
    • Solo con open source no se logró una buena adopción industrial; el producto de código cerrado y la capacitación y consultoría ayudaron a la adopción
  • Aunque aplicar pruebas basadas en propiedades solo a fragmentos de funciones puras ya puede aportar mucho valor, en los sistemas industriales abundan las databases, los stateful protocols y las concurrent data structures, por lo que las pruebas basadas en estado y paralelas tienen una importancia casi equivalente
  • Las especificaciones basadas en estado no siempre son más difíciles que las especificaciones con funciones puras
    • Un modelo de key-value store puede llegar bastante lejos solo con una lista de pares key-value
    • En el caso de LevelDB, un modelo simple encontró en pocos minutos un counterexample reducido de 17 pasos, y después de la corrección de Google volvió a encontrar en pocos minutos un counterexample de 31 pasos
    • El segundo problema era un bug en el background compaction process; la compaction es importante para mejorar el rendimiento de lectura y recuperar disk space, pero no estaba incluida explícitamente en el modelo
  • Aunque el código cerrado pudo haber ayudado a la adopción industrial, se evalúa que no ayudó a la adopción open source
  • Se considera que reproducir los resultados de los papers sin una licencia de Quviq QuickCheck requeriría mucho reverse engineering y sería casi imposible

Propuesta: una implementación pequeña y pública, y especificaciones fáciles

  • La dirección de mejora tiene dos partes
    • Ofrecer una implementación open source breve de pruebas basadas en propiedades con estado y paralelas, similar a la implementación original de QuickCheck de unas 300 líneas
    • Reducir la carga de escribir especificaciones reutilizando, en lugar de máquinas de estados, conceptos de mock y test double con los que los programadores ya están familiarizados
  • Para validar esta hipótesis se muestran dos cosas
    • Una implementación de pruebas basadas en propiedades con estado y paralelas en unas 400 líneas de código
    • El uso de una in-memory reference implementation, es decir, un fake, como modelo en lugar de una state machine

Resumen de las pruebas basadas en propiedades puras

  • En las pruebas de funciones puras, se generan entradas y se verifica que la salida de la función cumpla cierta relación con la entrada
  • Por ejemplo, reverse puede probarse con la propiedad reverse (reverse xs) == xs para una lista arbitraria xs
  • QuickCheck genera 100 pruebas por defecto y, si falla, reduce la entrada mediante shrinking para presentar un contraejemplo mínimo
  • Una propiedad incorrecta como reverse xs == xs se reduce a un contraejemplo mínimo como [0,1]
  • Los patrones de propiedades que aparecen con frecuencia incluyen inverse, idempotency, associativity, axiomas de abstract data types, metamorphic properties, etc.
    • inverse: deserialise (serialise i) == i
    • idempotency: sort (sort xs) == sort xs
    • associativity: (i + j) + k == i + (j + k)

Pruebas basadas en propiedades con estado

  • Los componentes con estado no siempre producen la misma salida para la misma entrada
    • El resultado del primer incr de un counter y el resultado del segundo incr dependen del estado previo
    • En una database y un file system, el historial de entradas previas también afecta la siguiente salida
  • Si las pruebas de funciones puras tratan con una sola entrada, las pruebas con estado generan secuencias de entradas para verificar cómo cambia el sistema con el tiempo
  • El modelo se expresa como un fake con la forma m -> i -> (m, o)
    • A partir del estado anterior del modelo m y la entrada i, se calculan el siguiente modelo y la salida o
    • En cada paso se compara la salida del sistema real con la salida del fake
    • Si no coinciden, se reduce la secuencia de entradas mediante shrinking para encontrar un contraejemplo pequeño

  • Ejemplo de counter

    • Se toma como sujeto de prueba un counter en Haskell que usa una variable mutable global
    • incr incrementa el counter y get lee el valor actual
    • Para el modelo basta un solo Counter Int, y la instancia de StateModel define el estado inicial Counter 0, Incr, Get, Incr_ (), Get_ Int, runFake, runReal y el generador de comandos
    • Si se introduce un bug que no incrementa cuando el valor del counter es 42, como incr42Bug, QuickCheck encuentra una falla tras 66 pruebas y, después de 29 shrinkings, presenta como contraejemplo mínimo hacer Get tras 43 incrementos
    • Si no se hace reset del counter global real entre pruebas, el modelo siempre empieza en 0, pero el counter real conserva el estado de la prueba anterior, lo que provoca un mismatch

  • Interfaz de bibliotecas para pruebas con estado

    • La interfaz StateModel ve el sistema bajo prueba como una black box y trata los comandos como entradas y las respuestas como salidas
    • Sus componentes principales son Command state, Response state, initialState, runFake, runReal y generateCommand
    • Los componentes opcionales son los siguientes
      • Reference: se usa cuando un comando posterior hace referencia a un recurso creado por una respuesta anterior, como un file handle
      • PreconditionFailure: representa fallas de precondición, por ejemplo impedir leer desde un handle que no corresponde a un archivo abierto
      • CommandMonad: por defecto es IO, pero se puede usar otro monad
      • monitoring, commandName: se usan para cobertura y estadísticas
    • Al generar comandos no se pueden crear valores como file handles reales, por lo que se generan referencias simbólicas con la forma Var Int y durante la ejecución se sustituyen por referencias reales
    • Después del shrinking, se eliminan los comandos que rompen precondiciones o usan referencias simbólicas fuera de scope

  • Ejemplo de circular buffer

    • Se prueba mediante Haskell FFI una circular queue escrita en C, y el modelo se escribe como una queue simple basada en listas
    • La implementación en C no hace error checking, por lo que hacer get en una queue vacía puede devolver memoria no inicializada
    • La implementación real es eficiente por usar índices circulares, pero no es obviamente correct; el fake es menos eficiente, pero no importa porque se usa para pruebas
    • Como new devuelve una referencia a la queue, el modelo administra varias queues con Map (Var Queue) FQueue
    • Al principio faltaba la precondición de hacer put en una queue llena, así que al poner 0 y 1 en una queue de tamaño 1 y hacer get, el modelo, por ser FIFO, esperaba 0, pero el código C devolvía 1
    • Esto no era un bug de implementación, sino la falta de una precondición en el modelo, y se corrige agregando la precondición QueueIsFull
    • La salida de cobertura reveló que faltaba el comando Size en el generador; al agregarlo, se descubrió un bug en el cálculo del tamaño de la queue
    • Si se pone un ítem en una queue de tamaño 1 y se hace Size, el valor esperado es 1, pero el valor real es 0; se propone corregirlo haciendo que new asigne un tamaño de buffer interno de n + 1
    • Luego abs(q->inp - q->outp) % q->size pasa para tamaño 1, pero vuelve a fallar con tamaño 2, y la corrección final es (q->inp - q->outp + q->size) % q->size

  • Puzzle de jarras de agua de Die Hard 3

    • Se resuelve con pruebas con estado el puzzle de obtener exactamente 4 L usando jarras de 3 L y 5 L
    • Incluso sin una implementación real, ejecutando solo el modelo y el fake se puede hacer que la prueba falle al alcanzar un estado específico para obtener una secuencia de acciones reducida
    • Tras 199 pruebas y 11 shrinkings, la secuencia presentada tiene el siguiente flujo
      • Llenar la jarra de 5 L
      • Verter de la jarra de 5 L a la de 3 L
      • Vaciar la jarra de 3 L
      • Volver a verter de la jarra de 5 L a la de 3 L
      • Llenar la jarra de 5 L
      • Verter de la jarra de 5 L a la de 3 L
    • La trace muestra los estados intermedios, lo que permite comprobar el proceso por el cual la jarra grande llega a tener 4 L

Pruebas basadas en propiedades en paralelo

  • Los bugs en código concurrente son difíciles de reproducir y de verificar que quedaron corregidos, porque el intercalado de threads cambia en cada ejecución.
  • El objetivo es permitir que los usuarios hagan pruebas en paralelo de forma similar a las pruebas secuenciales basadas en estado, sin tener que escribir mucho código de prueba adicional.
  • En el ejemplo del counter, si incr ejecuta readIORef y luego writeIORef de forma no atómica, dos threads pueden sobrescribir mutuamente sus incrementos y producir una race condition.
  • Las pruebas en paralelo recopilan los momentos de invocación y respuesta de los commands durante la ejecución para crear una historia concurrente, y verifican si esa historia puede explicarse mediante algún intercalado secuencial.
  • Si al menos un intercalado coincide con el modelo secuencial, se considera que la historia linearise y se la juzga correcta.
  • Si ningún intercalado secuencial puede explicar la respuesta real, se trata como un resultado no linearizable.

  • Generación y shrink de commands en paralelo

    • Un programa paralelo se representa con ParallelCommands y varios Fork, y los commands dentro de cada Fork se ejecutan en paralelo.
    • La implementación de ejemplo cubre ejecuciones con uno, dos y tres threads.
    • En una ejecución en paralelo, el estado posible del modelo puede variar según el intercalado, como en Fork [Write "a" "foo", Write "a" "bar"].
    • El modelo paralelo genera commands y realiza shrink en función de un conjunto de estados, no de un único estado.
    • parallelSafe verifica que la precondición se mantenga para todas las permutaciones de los commands dentro de un Fork.
    • Por ejemplo, si Write "a" y Delete "a" están en el mismo fork, un command puede romper la precondición del otro.
    • Durante el proceso de shrink, solo se conservan los commands que mantienen las precondiciones y el alcance de las referencias simbólicas.

  • Ejecución en paralelo y verificación de linearisability

    • La ejecución en paralelo registra los eventos Invoke y Ok de cada command en la historia.
    • Si una respuesta incluye una referencia nueva, el entorno se extiende con un contador atómico para evitar colisiones de números de referencia entre threads.
    • Todos los intercalados posibles de la historia se enumeran como un árbol Rose.
    • linearisable verifica si algún path de ese árbol hace coincidir el modelo secuencial runFake con la respuesta.
    • Como las pruebas en paralelo terminan reutilizando el modelo secuencial, el usuario escribe el modelo secuencial y obtiene pruebas en paralelo con poco código adicional.

  • Ejemplo de counter en paralelo

    • El único código agregado para activar las pruebas en paralelo del counter es la instancia ParallelModel Counter y una property.
    • Al usar el incrRaceCondition no atómico, se encuentra una race condition.
    • Aunque también haya una race en un test case más pequeño, si la falla no se reproduce por un intercalado distinto, QuickCheck puede considerar que el test case más pequeño pasa y detener el shrink.
    • La solución correcta es un thread scheduler determinista, y el paper sobre pruebas en paralelo lo usa.
    • La implementación de ejemplo usa como workaround más simple insertar un sleep breve alrededor de las lecturas/escrituras de memoria compartida, para aumentar la probabilidad de que ocurra el mismo intercalado.
    • El sleep no es necesario para encontrar la race, sino para reducir el counterexample encontrado.
    • Después de agregar el sleep, el contraejemplo mínimo se reduce a ParallelCommands [Fork [Incr,Incr],Fork [Get]].

  • Ejemplo de process registry

    • Como ejemplo se usa un sistema similar al process registry de Erlang, que spawnea threads y permite hacer register, lookup, unregister y kill de ThreadId por nombre.
    • El modelo secuencial rastrea los thread id creados, los pares nombre-thread registrados y los thread id eliminados.
    • Como Register y Unregister pueden fallar, se usa Either ErrorCall () en la respuesta.
    • La información de ubicación del error en la implementación real se elimina con abstractError para hacerla coincidir con la fake.
    • monitoring muestra la cobertura de RegisterFailed, RegisterSucceeded, UnregisterFailed y UnregisterSucceeded.
    • Si se introduce intencionalmente un bug en el que register sobrescribe el registry existente, aparece un contraejemplo secuencial donde no se puede hacer unregister de "e", que ya había sido registrado.
    • En las pruebas en paralelo aparece un contraejemplo más largo y, al usar SleepyIORef, se reduce a una forma como Fork [Register "b" (Var 0), Register "c" (Var 0)].
    • El problema es una race en la que otro thread puede interponerse entre la verificación con readRegistry y la llamada a atomicModifyIORef.
    • Después de aplicar un lock global a register, unregister y kill, las pruebas en paralelo pasan.

Modelo basado en fake y pruebas de integración

  • En lugar de una especificación tradicional de máquina de estados con postcondiciones, se usa un fake en memoria como implementación de referencia
  • El artículo de 2019 de Edsko de Vries se presenta como el primero en proponer una forma de implementar un fake sobre una especificación de máquina de estados basada en postcondiciones
  • El fake es parecido a un mock, por lo que se plantea como un enfoque más accesible para programadores que no están acostumbrados a las especificaciones formales
  • Un fake también tiene la ventaja de poder usarse en pruebas de integración en lugar de componentes dependientes
    • No hace falta iniciar ni habilitar la dependencia real
    • Permite construir pruebas de integración más rápidas y deterministas
  • El problema de que el fake pueda estar equivocado se aborda con contract tests
  • Como las pruebas basadas en propiedades con estado y en paralelo verifican que el fake y la implementación real coincidan, el fake actúa como una dependencia validada por pruebas de contrato

  • Separar pruebas y despliegue con un fake de Queue

    • La interfaz de queue IQueue tiene iNew, iPut, iGet, iSize
    • La implementación real conecta directamente el wrapper de C queue
    • La implementación fake guarda el estado del modelo en un IORef y lo actualiza mediante fNew, fPut, fGet, fSize
    • El componente se escribe contra la interfaz IQueue q
    • En las pruebas se usa la instancia fake, y en el despliegue se usa la instancia real
    • Con pruebas basadas en propiedades con estado se establece la premisa de que el fake es fiel al real

  • Fake de file system

    • La interfaz de file system IFileSystem h tiene iMkDir, iOpen, iWrite, iClose, iRead
    • La implementación real usa el file system real bajo /tmp/qc-test
    • El fake se implementa como un FakeFS en memoria con un conjunto de directorios, un mapa de contenidos de archivos, un mapa de handles abiertos y el siguiente handle
    • fOpen, fWrite, fClose, fRead modelan fallas de precondición como archivo ocupado, directorio inexistente o handle cerrado
    • Si se prueba que el file system fake es fiel al file system real, los componentes que dependen del file system pueden probarse en integración con el fake y reemplazarse por el file system real al desplegar
    • Si al reemplazarlo por el real aparece un bug, hay que investigar cómo el mismatch entre el fake y el real logró pasar las pruebas basadas en propiedades con estado

  • Sistemas de componentes más grandes

    • Un sistema donde A depende de B y B depende de C también se extiende de la misma manera
    • Se define una interfaz para cada componente
      • iC :: IO IC
      • iB :: IC -> IO IB
      • iA :: IB -> IO IA
    • La estrategia de prueba es la siguiente
      • Verificar C con pruebas basadas en propiedades con estado y en paralelo para obtener un fake C validado por contrato
      • En las pruebas de integración de B se usa el fake C
      • En las pruebas de A se usa un fake B que usa el fake C
    • Este enfoque se extiende con el mismo patrón a más componentes o servicios

Conclusión

  • Las pruebas basadas en propiedades con estado y en paralelo pueden implementarse con unas 400 líneas de código, una escala comparable con la primera implementación de QuickCheck, que tenía unas 300 líneas y no incluía shrinking
  • Usar un fake como modelo convierte la escritura de especificaciones para pruebas con estado y en paralelo en algo más familiar, y permite reutilizarlas para probar sistemas más grandes de forma composicional
  • Si cada comunidad de lenguaje sigue experimentando, hay margen para mejorar el estado de las bibliotecas de pruebas basadas en propiedades

Lecturas relacionadas

1 comentarios

 
GN⁺ 2024-07-06
Opiniones de Hacker News

  • Me da curiosidad qué se pierde uno si no usa una biblioteca de pruebas basadas en propiedades, dado que ya existe el fuzzing basado en cobertura y Go lo soporta bastante bien
    https://www.tedinski.com/2018/12/11/fuzzing-and-property-tes...
    Al ver la prueba de fuzzing de abajo y la verificación de invariantes correspondiente, me parece que en la práctica es casi lo mismo que una prueba de propiedades
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...

    • La distinción entre pruebas basadas en propiedades y fuzzing es, en general, más bien una agrupación aproximada por estilo
      Hay diferencias reales, pero los límites son bastante difusos, y no es tan importante trazar una línea exacta entre qué es fuzzing y qué es prueba basada en propiedades
      Las pruebas rápidas y con aserciones detalladas son pruebas basadas en propiedades; lo que corre durante mucho tiempo y solo busca fallos suele ser fuzzing; lo que queda en medio es ambiguo
      https://hypothesis.works/articles/what-is-property-based-tes...
    • El fuzzing basado en cobertura y las pruebas basadas en propiedades pueden combinarse perfectamente
      Cuando estaba en Google, había una herramienta interna que combinaba ambas cosas y era realmente buena. Escribías pruebas basadas en propiedades como de costumbre y, al ejecutarlas, el framework de pruebas compilaba de forma especial para obtener cobertura y ajustaba las entradas aleatorias para aumentarla. Por supuesto, corría de manera totalmente automática en un clúster de varias máquinas
      Las pruebas basadas en propiedades tradicionales normalmente se implementan solo como bibliotecas, así que no necesariamente cuentan con información de cobertura para guiar la generación de entradas aleatorias
    • Como estás haciendo aserciones sobre propiedades, diría que por definición cuenta como prueba basada en propiedades, del tipo “todos los nodos con nivel mayor que 1 tienen dos hijos”
      Dicho eso, según la biblioteca puedes obtener bastantes funciones convenientes. Una de las útiles es el shrinking, y puedes consultar la sección “Shrinking” aquí: https://tech.fpcomplete.com/blog/quickcheck-hedgehog-validit...
      Los combinadores para componer generadores también son excelentes, y según la biblioteca a veces incluso incluyen conjuntos conocidos de valores “malos” que provocan comportamientos excepcionales
    • No tengo muy claro en qué se diferencian las pruebas de fuzzing de Go de lo que dice el artículo enlazado, pero allí se afirma que un fuzzer de verdad debe ejecutarse durante días o semanas, y que casi siempre hay que elegir pruebas basadas en propiedades antes que fuzzing
      Quisiera dar un paso atrás y plantear una pregunta más meta sobre las pruebas. ¿Que una prueba pase significa que el código es correcto, y también lo contrario? ¿Hay alguna parte del contrato de Go que especifique que, si se le da la misma entrada al mismo código, se obtiene la misma salida?
    • Desde el punto de vista de la API, lo que se obtiene principalmente es una biblioteca de combinadores para generar las estructuras de datos aleatorias que uno quiere
      Al trabajar con el tipo Arbitrary, que representa un conjunto de objetos aleatorios, es fácil escribir funciones reutilizables para generar entradas de prueba. Una biblioteca así probablemente podría usarse con bastante facilidad junto con el framework de fuzzing de Go
      Aun así, creo que combinadores comunes como map, filter, chain y oneOf pueden resultar algo incómodos, así que estoy escribiendo una nueva biblioteca de pruebas de propiedades para JavaScript. El objetivo es hacerla más agradable de usar, pero todavía es experimental y no se ha publicado

  • clojure.spec.alpha fue una experiencia excelente, ya fuera usándolo junto con test.check o no, pero al probar hypothesis de Python fue realmente pésimo
    Hypothesis parecía no poder manejar, por diseño, conjuntos de datos simples pero “grandes”, y aquí “grande” en realidad tampoco es tan grande. [0] Fue tan doloroso que terminé quitando por completo Hypothesis y las pruebas basadas en generación del conjunto de pruebas de Python en el trabajo
    [0] https://github.com/HypothesisWorks/hypothesis/issues/3493

    • En este caso, más que que Hypothesis no pueda manejar conjuntos de datos grandes, suena a que estaba rechazando muchos de los casos reducidos
      Hypothesis intentaba reducir los enteros generados a 0 para ver si el bug también existía con 0, y la prueba, en lugar de fallar, los rechazaba por contener 0. En casos pequeños solo era ineficiente, pero en casos grandes llegó al punto de que Hypothesis se rendía
      En ese hilo, alguien sugirió usar otra estrategia de generación de instancias que no pudiera generar 0. Es decir, no generar el valor favorito del reductor de Hypothesis para luego rechazarlo, sino no generarlo desde el principio. Me da curiosidad si lo intentaron
      También me da curiosidad cómo clojure.spec.alpha maneja esto de forma distinta
      En el comentario de mjaniczek en https://news.ycombinator.com/item?id=40876437 se señala este caso como una desventaja del enfoque de Hypothesis
      La idea es: “el generador ahora se convierte en un parser de listas de bytes que puede fallar, así que aparece algo de ineficiencia, y el usuario puede crear generadores raros que el reductor interno no logra reducir perfectamente. Aun así, de los tres enfoques, es el que ofrece la mejor experiencia de desarrollador…”
      Claro que probablemente no estaría de acuerdo con que escribiste tu prueba de una forma “rara”
    • Me gustaba que spec de Clojure fuera realmente fácil de armar alrededor de otras cosas, pero al pasarme a Elixir, para escribir pruebas de ese tipo tuve que bajar hasta propEr, una vieja biblioteca de Erlang. Bastante decepcionante
    • El ejemplo del issue de GitHub usa filter de una forma que se provoca su propio problema
      Si generas algo al azar y luego filtras lo que cumple cierta propiedad, en la práctica estás raspando un boleto de lotería durante la generación

  • La respuesta simple a la pregunta del texto: “¿por qué no existe el requisito de que las investigaciones publicadas deban ser reproducibles con herramientas open source, o al menos con herramientas disponibles gratis para el público y otros investigadores?”, es que la consecuencia inmediata de tal requisito sería que los papers que no cumplan esa condición no se publicarían
    Por ejemplo, tampoco se habría publicado algo como el paper de Quviq QuickCheck, que parece haber sido útil para sus autores y para otras personas, y la comunidad habría perdido el regalo de esa información

    • Me gustaría que algunas editoriales exigieran reproducibilidad y otras no
      Todo requisito tiene un efecto excluyente, y siempre hay casos límite de papers que pueden ser útiles aunque no cumplan los requisitos
    • Esta no es una pregunta con una respuesta clara y tajante, e incluso podría llamarse una pregunta política, pero aun así esa línea de defensa no es muy válida
      Si damos por válida esa lógica, se puede usar como escudo para llegar a cualquier extremo. Si se elimina la reproducibilidad como requisito, no hace falta explicar nada que no se quiera explicar. No hay que proporcionar datos sobre la muestra ni pruebas de significancia estadística. Basta con un abstract vago que afirme haber logrado algún resultado
      Incluso la famosa nota que Fermat dejó en el margen de su copia personal de la Arithmetica se convertiría en un paper de investigación totalmente válido. Al fin y al cabo, no querríamos perder la valiosa información de que un matemático famoso creía tener una prueba concisa y elegante de cierto teorema. Aunque, por supuesto, lo más probable es que en realidad no la tuviera
      Mi postura sobre esta pregunta política es que los estándares actuales son demasiado laxos. Nadie está obligado a publicar nada. Hay mucha investigación en el mundo que no se publica en ningún lado por razones como su valor propietario, y esa investigación no va a desaparecer
      Pero si trabajas en la academia y, más aún, recibes financiamiento para investigación, y dices que tu objetivo es hacer avanzar el conocimiento científico del mundo, es justo exigir que realmente sigas ese objetivo. No que solo finjas seguirlo para subir por la escalera de la carrera académica
    • Creo que también podría ser viable revelar el código fuente solo a los revisores
      Junto con todo lo necesario para ejecutar el código. Quizás ya lo estén haciendo así
    • Porque la reproducibilidad es una piedra angular del método científico
    • Los papers se publican porque sus autores quieren aumentar su “índice de importancia”, y eso está conectado de forma muy directa con la remuneración y las posibilidades de carrera académica
      Es poco probable que agregar más requisitos con ese fin reduzca la cantidad de papers publicados
      El problema más grave de los papers publicados es que, para publicar lo más posible y lo más rápido posible, a menudo se pasan por alto los errores deliberadamente. Si verificar los papers se vuelve más fácil, quizá esta situación mejore, pero no tendría demasiadas expectativas. La gente es muy buena encontrando atajos

  • Con proptest de Rust escribo pruebas de propiedades con estado con bastante frecuencia, y normalmente las programo a mano; es bastante sencillo.
    Un ejemplo no trivial que encontró 6 bugs está en https://github.com/sunshowers-code/buf-list/blob/main/src/cu...
    Las pruebas en paralelo pueden ser útiles a veces, pero muchas veces es más fácil simplemente correr muchas pruebas en paralelo.

    • En Rust escribo muchas pruebas de propiedades manuales, y por lo general tienen esta forma:
      En el nivel superior uso aleatoriedad real, y debajo pongo varios bucles anidados que van de casos de baja complejidad a casos de mayor complejidad. Luego genero e imprimo una semilla para dársela a un generador pseudoaleatorio determinista. Si la prueba falla, basta con copiar y pegar la semilla del error para reproducir el caso fallido.
      Siento que estas pruebas de propiedades manuales son más rápidas, más flexibles y, en general, menos engorrosas que cualquier framework o biblioteca.
      Eso sí, para pruebas de concurrencia realmente robustas recomiendo mucho la biblioteca AWS Shuttle (https://github.com/awslabs/shuttle). Puede encontrar condiciones de carrera increíblemente complejas. También escribí un pequeño tutorial: https://grantslatton.com/shuttle
      En AWS la usaron para validar un sistema de archivos personalizado que escribieron para operar AWS S3.

  • Le eché un vistazo rápido al paper enlazado “Testing Telecoms Software with Quviq QuickCheck”, pero no vi de inmediato una respuesta a la pregunta: “¿por qué no sería mejor construir uno mismo esta operación con estado?”
    El texto original apunta a esta parte con el modelo de pares clave-valor de un almacén clave-valor, pero no entiendo por qué no simplemente escribir una máquina de estados, ni por qué hace falta un framework. La semana pasada, en el trabajo, hice literalmente eso para probar interacciones con un sistema de archivos, y al final se redujo a algo como type Instruction = | Read of stuff | Write of stuff | Seek of stuff | …
    Entonces la propiedad pasa a ser “dada esta lista de comandos, …”. El tipo StateModel básicamente pide lo mismo. Cuesta ver que StateModel aporte lo suyo, y parece que solo elimina una cantidad muy pequeña de código de prueba en la práctica, a cambio de agregar mucho más código de framework que hay que entender.

    • Hay pruebas en las que ese juicio es correcto, pero la parte de reducir los casos fallidos suele ser complicada.
      Si quieres generar solo secuencias de transiciones de estado “válidas”, normalmente necesitas un estado de modelo que determine qué paso de prueba es válido en un estado específico. Además, durante la reducción, al eliminar pasos de prueba, hay que evitar romper las precondiciones que se respetaron al generar originalmente cada paso, para no producir fallos falsos.
      Si en cualquier estado cualquier operación es válida y solo quieres una secuencia totalmente aleatoria de operaciones arbitrarias, un framework de proptest con estado puede ser excesivo. Pero si necesitas mantener estado de modelo y especificar precondiciones para varias operaciones, un framework dedicado te ahorra mucho trabajo.
      El año pasado escribí un post sobre este tema; si te interesa un ejemplo más profundo, puede servirte: https://readyset.io/blog/stateful-property-testing-in-rust
      Como dijeron otros, las pruebas de máquinas de estado en paralelo también son una ventaja interesante que se obtiene con un framework dedicado, pero no es la única.
    • Creo que la parte con estado la cubren mejor las pruebas basadas en modelos.
      Puedes mezclar estilos de prueba. Es tu código.
    • Entiendo que QuickCheck en paralelo verifica que todos los intercalados posibles en un programa multihilo terminen produciendo estados a los que también se podría llegar llamando los comandos de forma secuencial.
      Esa es la ventaja.

  • El autor se concentra en los aspectos de máquinas de estado y paralelismo de las pruebas basadas en propiedades, pero hay otros aspectos que podrían tener un impacto mayor.
    Uno es el testing basado en propiedades guiado por cobertura, y basta con ver el artículo de Dan Luu: https://danluu.com/testing/
    Otro es el lado hacia el que yo estoy sesgado: automatizar el encogimiento manteniendo todas las invariantes creadas al generar los valores.
    En resumen, las funciones de encogimiento derivadas al estilo QuickCheck que operan sobre valores (shrink : a -> [a]) tienen restricciones y problemas, lo que hace que la gente termine desactivando el encogimiento en lugar de lidiar con el problema.
    El “encogimiento integrado” con árboles rose (por ejemplo, Hedgehog) respeta las restricciones del generador, pero tiene problemas con el bind monádico, es decir, cuando se usa el resultado de un generador para ramificar hacia otro generador.
    El único enfoque que mágicamente parece “simplemente funcionar” es el encogimiento interno de Hypothesis. Usa una capa de indirección que reduce una lista de elecciones aleatorias, no el valor en sí. La desventaja es que el generador ahora se convierte en un parser de listas de bytes que puede fallar, lo que introduce cierta ineficiencia, y que los usuarios pueden crear generadores raros que el encogedor interno no logra reducir perfectamente. Aun así, de los tres enfoques es el que ofrece la mejor experiencia de desarrollo y, considerando que ya es un pequeño milagro que la gente escriba tests, como autor de una biblioteca de testing parece el enfoque que más vale la pena construir.

    • Sobre la parte de que el “encogimiento integrado” con árboles rose (por ejemplo, Hedgehog) respeta las restricciones del generador pero tiene problemas con el bind monádico: dentro de los límites de mi conocimiento amateur, lo veo como una limitación fundamental de bind monádico/generador.
      En cambio, para un encogimiento óptimo habría que preferir generadores applicative: https://github.com/hedgehogqa/haskell-hedgehog/issues/473#is...
      En otras palabras, los generadores applicative no “usan el resultado de un generador para ramificar hacia otro generador”, y debido al carácter “paralelo” de applicative, el encogimiento se optimiza. Aquí paralelo no se refiere al sentido de threading del artículo, sino al sentido monádico. Como applicative es “paralelo”, los generadores pueden reducirse de forma independiente. En cambio, un generador monádico es “serial”, así que reducir uno necesariamente cambia el comportamiento del generador que le sigue.
      Si hay una charla pública, me gustaría ver el enlace.
    • Personalmente, Hypothesis estuvo lejos de “simplemente funcionar”.
      No creo que esté realmente listo para producción, y además parece que es así por diseño.[0]
      Tenía bastante experiencia usando clojure.spec.alpha, con y sin test.check, así que aunque haya diferencias, no estaba completamente ajeno a la idea general.
      [0] https://github.com/HypothesisWorks/hypothesis/issues/3493
    • Mi framework preferido es falsify, que ofrece “encogimiento integrado interno”.
      Es parecido a Hypothesis, pero usa un árbol de generadores en lugar de una secuencia lineal. Se basa en funtores selectivos (selective functors), que son una buena interfaz también útil para cosas como validadores.
      Según https://hackage.haskell.org/package/falsify, esta biblioteca ofrece testing basado en propiedades con soporte para encogimiento integrado interno. Integrado en el sentido de Hedgehog, es decir, que no hace falta escribir por separado un encogedor y un generador; e interno en el sentido de Hypothesis, es decir, que también funciona bien a través de bind monádico.

  • Intenté usar testing basado en propiedades, pero siempre sentí que quedaba entre dos aguas.
    Si entiendo una propiedad lo bastante bien como para testearla con rigor, normalmente puedo empujarla al sistema de tipos y hacer que sea verdadera por construcción. Si solo quiero una prueba de humo sencilla, un input arbitrario es más fácil.

    • Me da curiosidad qué tipo de propiedades tenías en mente.
      Por ejemplo, muchas veces tienes dos implementaciones, una ingenua lenta pero simple y otra optimizada, y puedes comparar sus salidas para entradas arbitrarias. Es una propiedad simple y fácil de entender, pero en general es difícil meterla en el sistema de tipos.
      Del mismo modo, puede ser que el orden en que se presentan las entradas no deba importar, o que haya una forma de dividir los datos y se cumpla algo como max(máximo de A, máximo de B) = maximum(A union B). ¿Cómo se podría codificar eso en el sistema de tipos?
      O cosas como “para A y B arbitrarios, alguna solución óptima encontrada en A es peor que alguna solución óptima encontrada en A union B”, o idempotencia como f(f(A)) = f(A).
      Todas estas son propiedades fáciles de entender, pero no son fáciles de expresar en la mayoría de los sistemas de tipos.
    • Si es posible, claramente es mejor imponer las restricciones en tiempo de compilación.
      Pero hay muchas restricciones que los verificadores de tipos mainstream no pueden manejar. Los tipos dependientes ayudarían mucho, pero todavía parecen estar limitados a nichos como los demostradores de teoremas.

  • Me pregunto si no falta en la lista el QuviQ Erlang QuickCheck original.
    El producto completo es propietario, pero también ofrecen QuickCheck Mini, una versión gratuita: http://www.quviq.com/downloads/

  • Clojure ahora también tiene una biblioteca quickcheck con estado: https://github.com/griffinbank/test.contract
    El testing paralelo es interesante, pero todavía no ha sido una gran fuente de dolor.

  • Para pruebas en C#/.NET venía usando CsCheck[0] y quedé bastante conforme
    Era mucho más accesible que Hedgehog o FsCheck, y también bastante rápido
    [0] https://github.com/AnthonyLloyd/CsCheck