true - ¿Cuál es el significado de una suposición en scala en comparación con una afirmación?

scalatest matchers true

Question

Scala parece definir 3 tipos de afirmaciones: assert , require y assume .

Por lo que puedo entender, la diferencia (en comparación con una aserción genérica) de require es que está específicamente destinado a verificar entradas (argumentos, mensajes entrantes, etc.). ¿Y cuál es el significado de assume entonces?

Answer 1

Si miras el código en Predef.scala , verás que los tres hacen un trabajo muy similar:

def assert(assertion: Boolean) { 
  if (!assertion) 
    throw new java.lang.AssertionError("assertion failed") 
} 

def assume(assumption: Boolean) { 
  if (!assumption) 
    throw new java.lang.AssertionError("assumption failed") 
} 

def require(requirement: Boolean) { 
  if (!requirement) 
    throw new IllegalArgumentException("requirement failed") 
} 

También hay versiones que toman argumentos adicionales para los informes (ver http://harrah.github.com/browse/samples/library/scala/Predef.scala.html ).

La diferencia está en el tipo de excepción que arrojan y el mensaje de error que generan.

Sin embargo, los inspectores estáticos podrían tratar a los tres de manera diferente. La intención es que assert especifique una condición que una comprobación estática debe intentar demostrar, assume que se utilizará para una condición que el verificador puede suponer que contenga, mientras que require especificar una condición que la persona que llama debe garantizar. Si un verificador estático encuentra una violación de assert lo considera un error en el código, mientras que cuando se infringe se supone que la persona que llama tiene la culpa.

Answer 2

La diferencia

La diferencia entre assert () y assume () es que

• assert () es una forma de documentar y verificar dinámicamente invariantes, mientras
• assume () está destinado a ser consumido por herramientas de análisis estático

El consumidor / contexto previsto de assert () está probando, como una prueba JUnit de Scala, mientras que el de assume () es "como un medio de especificación de estilo de diseño por contrato de las condiciones previas y posteriores de las funciones, con el intención de que estas especificaciones puedan ser consumidas por una herramienta de análisis estático "(extraído del scaladoc ).

Análisis estático / comprobación de modelo

En el contexto del análisis estático, como ha señalado Adam Zalcman, assert () es una aserción de todos los caminos de ejecución, para verificar una invariante global, mientras que assume () funciona localmente para reducir la cantidad de comprobación que el analizador necesita hacer. asumir () se usa en el contexto del razonamiento de suponer garantía, que es un mecanismo de dividir y conquistar para ayudar a los inspectores modelo a suponer algo sobre el método para abordar el problema de explosión de estado que surge cuando se intenta verificar todas las rutas que el programa puede tomar. Por ejemplo, si usted sabía que en el diseño de su programa, una función f1 (n1: Int, n2: Int) NUNCA pasaba n2 <n1, entonces al afirmar esta suposición explícitamente ayudaría al analizador a no tener que verificar MUCHAS combinaciones de n1 y n2.

En la práctica

En la práctica, dado que tales correctores de modelo de programa completo siguen siendo principalmente teóricos, veamos lo que hace el compilador e intérprete de scala:

1. ambas expresiones assume () y assert () se verifican en tiempo de ejecución
2. -Xdisable-assertions inhabilita la comprobación de assume () y assert ()

Más

Más del excelente scaladoc sobre este tema:

Afirmaciones

Se proporciona un conjunto de funciones afirmativas para usarlas como una forma de documentar y verificar dinámicamente invariantes en el código. las sentencias assert se pueden elidir en el tiempo de ejecución proporcionando el argumento de línea de comando -Xdisable-assertions al comando scala .

También se proporcionan variantes de assert destinadas a ser utilizadas con herramientas de análisis estático: assume , require y ensuring . require y aseguran su uso como un medio de especificación de estilo de diseño por contrato de las condiciones previas y posteriores de las funciones, con la intención de que estas especificaciones puedan ser consumidas por una herramienta de análisis estático. Por ejemplo,

def addNaturals(nats: List[Int]): Int = {
  require(nats forall (_ >= 0), "List contains negative numbers")
  nats.foldLeft(0)(_ + _)
} ensuring(_ >= 0)

La declaración de addNaturals establece que la lista de enteros aprobada solo debe contener números naturales (es decir, no negativos) y que el resultado devuelto también será natural. require es distinto de assert en el sentido de que si la condición falla, entonces la persona que llama de la función tiene la culpa en lugar de un error lógico que se haya hecho dentro de addNaturals. asegura es una forma de afirmación que declara la garantía que la función proporciona con respecto a su valor de retorno. )

Answer 3

En segundo lugar respondo Adams, aquí hay algunas pequeñas adiciones:

Cuando se viola la assume , la herramienta de verificación corta silenciosamente la ruta, es decir, no sigue la ruta más profundamente.

Por lo tanto, assume que a menudo se usa para formular precondiciones, assert para formular condiciones posteriores.

Estos conceptos son utilizados por muchas herramientas, por ejemplo, la herramienta de pruebas concólicas KLEE , herramientas de verificación de modelos acotadas por software como CBMC y LLBMC , y en parte también por herramientas de análisis de código estático basadas en la interpretación abstracta. El artículo Encontrar un terreno común: Elegir, Afirmar, Asumir presenta estos conceptos e intenta estandarizarlos.