Quelle est la signification d'une hypothèse en scala par rapport à une assertion ?

Question

Scala semble définir 3 types d'assertions : assert , require y assume .

Pour autant que je puisse comprendre, la différence (par rapport à une assertion générique) de require est qu'il est spécifiquement destiné à vérifier les entrées (arguments, messages entrants, etc.). Et quelle est la signification de assume alors ?

Answer 1

Si vous regardez le code dans Predef.scala vous verrez que les trois font un travail très similaire :

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") 
} 

Il existe également des versions qui prennent des arguments supplémentaires à des fins de rapport (cf. http://harrah.github.com/browse/samples/library/scala/Predef.scala.html ).

La différence réside dans le type d'exception qu'ils lèvent et le message d'erreur qu'ils génèrent.

Toutefois, les vérificateurs statiques pourraient traiter ces trois éléments différemment. L'intention est que assert pour spécifier une condition qu'une vérification statique doit tenter de prouver, assume doit être utilisé pour une condition que le vérificateur peut supposer vérifiée, tandis que require spécifie une condition que l'appelant doit assurer. Si un vérificateur statique trouve une violation de assert il considère qu'il s'agit d'une erreur dans le code, alors que lorsque require est violé, il suppose que l'appelant est en faute.

Answer 2

La différence

La différence entre assert() et assume() est que

• assert() est un moyen de documenter et de vérifier dynamiquement les invariants, tandis que
• assume() est destiné à être utilisé par les outils d'analyse statique.

Le consommateur / contexte prévu de assert() est le test, tel qu'un test JUnit Scala, tandis que celui de assume() est "un moyen de spécification de style conception par contrat des pré et post-conditions sur les fonctions, avec l'intention que ces spécifications puissent être consommées par un outil d'analyse statique" (extrait de l scaladoc ).

Analyse statique / vérification du modèle

Dans le contexte de l'analyse statique, comme Adam Zalcman l'a souligné, assert() est une assertion pour tous les chemins d'exécution, pour vérifier un invariant global, tandis que assume() travaille localement pour réduire la quantité de vérification que l'analyseur doit faire. assume() est utilisé dans le contexte du raisonnement assume-guarantee, qui est un mécanisme de division et de conquête pour aider les vérificateurs de modèles à supposer quelque chose sur la méthode afin de s'attaquer au problème d'explosion d'état qui se pose lorsqu'on essaie de vérifier tous les chemins que le programme peut prendre. Par exemple, si vous saviez que dans la conception de votre programme, une fonction f1(n1 : Int, n2:Int) n'est JAMAIS passée n2 < n1, alors énoncer cette hypothèse explicitement aiderait l'analyseur à ne pas avoir à vérifier BEAUCOUP de combinaisons de n1 et n2.

En pratique

En pratique, puisque de tels vérificateurs de modèles de programmes entiers sont encore essentiellement théoriques, examinons ce que font le compilateur et l'interpréteur scala :

1. les expressions assume() et assert() sont vérifiées au moment de l'exécution.
2. -Xdisable-assertions désactive la vérification de assume() et assert().

Plus de

L'excellent scaladoc nous en dit plus sur ce sujet :

Assertions

Un ensemble de assert sont fournies pour être utilisées comme un moyen de documenter et de vérifier dynamiquement les invariants dans le code. Les déclarations assert peuvent être élidées au moment de l'exécution en fournissant l'argument de la ligne de commande -Xdisable-assertions a la scala commandement.

Variantes de assert destinés à être utilisés avec des outils d'analyse statique sont également fournis : assume , require y ensuring . require et garantissant sont destinés à être utilisés comme un moyen de spécification de type conception par contrat des pré et post-conditions sur les fonctions, avec l'intention que ces spécifications puissent être consommées par un outil d'analyse statique. Par exemple,

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

La déclaration de addNaturals indique que la liste des entiers passés ne doit contenir que des nombres naturels (c'est-à-dire non négatifs) et que le résultat renvoyé sera également naturel. require se distingue de assert en ce sens que si la condition échoue, c'est l'appelant de la fonction qui est à blâmer plutôt qu'une erreur logique commise dans addNaturals elle-même. ensures est une forme de assert qui déclare la garantie que la fonction fournit en ce qui concerne sa valeur de retour. )

Answer 3

Je soutiens la réponse d'Adams, voici juste quelques petits ajouts :

Quand assume est violée, l'outil de vérification élague silencieusement le chemin, c'est-à-dire qu'il ne suit pas le chemin plus profondément.

Par conséquent, assume est souvent utilisé pour formuler des pré-conditions, assert pour formuler des post-conditions.

Ces concepts sont utilisés par de nombreux outils, par exemple l'outil de test concolique KLEE des outils de vérification de modèles limités par logiciel comme CBMC y LLBMC et en partie aussi par des outils d'analyse statique du code basés sur l'interprétation abstraite. L'article Trouver un terrain d'entente : Choisir, Affirmer, Assumer introduit ces concepts et tente de les normaliser.