В чем смысл предположения в скале по сравнению с утверждением? - PullRequest
Новая
       11

В чем смысл предположения в скале по сравнению с утверждением?

43 голосов
/ 04 ноября 2011

Скала, кажется, определяет 3 вида утверждений: assert, require и assume.

Насколько я понимаю, разница (по сравнению с общим утверждением) составляет requireявляется то, что он специально предназначен для проверки входных данных (аргументы, входящие сообщения и т. д.).А в чем смысл assume тогда?

Ответы [ 3 ]

49 голосов
/ 04 ноября 2011

Если вы посмотрите на код в Predef.scala, вы увидите, что все три выполняют очень похожую работу: 

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

Существуют также версии, которые принимают дополнительные аргументы для целей отчетности (см. http://harrah.github.com/browse/samples/library/scala/Predef.scala.html).

Разница заключается в типе исключения, которое они генерируют, и в сообщении об ошибке, которое они генерируют.

Однако статические контролеры могут обрабатывать все три по-разному. Намерение assert - указать условие, чтоСтатическая проверка должна попытаться доказать, assume должен использоваться для условия, которое может выполнять проверка, в то время как require указывает условие, которое должен обеспечить вызывающий объект. Если статическая проверка находит нарушение assert, этосчитает это ошибкой в ​​коде, в то время как при нарушении require предполагается, что вызывающий абонент виноват.

19 голосов
/ 20 октября 2013

разница

Разница между assert () и предположить () заключается в том, что

  • assert () - это способ документировать и динамически проверять инварианты, а
  • предположим, что () предназначен для использования инструментами статического анализа

Предполагаемый потребитель / контекст assert () - это тестирование, такое как тест Scala JUnit, в то время как тест предположения () - это «как средство спецификации стиля по контракту предварительных и постусловий для функций». с намерением, чтобы эти спецификации могли быть использованы инструментом статического анализа "(выдержка из scaladoc ).

Статический анализ / проверка модели

В контексте статического анализа, как указал Адам Залкман, assert () является утверждением всех путей выполнения, чтобы проверить глобальный инвариант, тогда как accept () работает локально, чтобы сократить объем проверки того, что анализатор нужно сделать. accept () используется в контексте рассуждения о предположении-гарантии, который является механизмом «разделяй и властвуй», чтобы помочь контролерам моделей принять что-то в методе для решения проблемы взрыва состояний, возникающей при попытке проверить все пути, которые программа может занять. Например, если вы знали, что при разработке вашей программы функция f1 (n1: Int, n2: Int) НИКОГДА не передается n2

На практике

На практике, поскольку такие контроллеры моделей для всей программы все еще в основном теоретические, давайте посмотрим, что делает компилятор и интерпретатор scala:

  1. оба предположения () и выражения assert () проверяются во время выполнения
  2. -Xdisable-assertions отключает проверку как предположить (), так и проверки assert ()

Подробнее

Больше от превосходного скаладока на эту тему:

* 1034 утверждения *

Набор функций assert предоставляется для использования в качестве способа документирования и динамической проверки инвариантов в коде. Операторы assert можно исключить во время выполнения, указав аргумент командной строки -Xdisable-assertions для команды scala.

Также предусмотрены варианты assert, предназначенные для использования с инструментами статического анализа: assume, require и ensuring. require и обеспечение предназначены для использования в качестве средства определения стиля по контракту предварительных и постусловий функций с намерением использования этих спецификаций инструментом статического анализа. Например, 

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

Объявление addNaturals гласит, что список переданных целых чисел должен содержать только натуральные числа (то есть неотрицательные), и что возвращаемый результат также будет натуральным. Требование отличается от утверждения в том, что если условие не выполняется, то виноват вызывающий функции, а не логическая ошибка, сделанная в самой addNaturals. обеспечивает это форма утверждения, которая объявляет гарантию, которую функция предоставляет относительно ее возвращаемого значения. )

5 голосов
/ 21 февраля 2015

Я второй ответ Адамса, вот лишь несколько небольших дополнений:

Когда нарушается assume, инструмент проверки молча сокращает путь, т. Е. Не следует по пути глубже.

Следовательно, assume часто используется для формулировки предварительных условий, assert для формулирования постусловий.

Эти понятия используются многими инструментами, например, инструмент для конколического тестирования KLEE , программно-ограниченные инструменты проверки моделей, такие как CBMC и LLBMC , а также частично с помощью инструментов статического анализа кода на основе абстрактной интерпретации. В статье Нахождение точки соприкосновения: выбери, утверждай, предполагай вводит эти понятия и пытается их стандартизировать.

...