Проверка основных операций над множествами в JML - PullRequest
Новая
       56

Проверка основных операций над множествами в JML

0 голосов
/ 03 октября 2019

Как проверить основные операции над множествами, такие как пересечение, объединение и различие в инструменте JML, таком как OpenJML, в котором ключевые слова, такие как "\ intersect \ set_minus \ set_union", не поддерживаются?

Интерфейсы Java, на которых яхотите сделать проверку на выглядит так: 

MySetInterface<S> intersect (MySetInterface<S> set)
MySetInterface<S> union (MySetInterface<S> set)
MySetInterface<S> difference (MySetInterface<S> set)

1 Ответ

1 голос
/ 04 октября 2019

Вам нужно будет найти функциональное описание для этих операций, как и для всех методов, которые не имеют прямого соответствия в теориях, поддерживаемых JML. Например, математическое определение объединения двух наборов - это «набор всех объектов, которые являются членами одного или другого набора». То есть метод union может быть указан примерно как 

/*@ public normal_behavior
  @ ensures this.containsAll(\old(this)) &&
  @         this.containsAll(\old(set)); */

и аналогично для других методов, при условии, что доступен чистый метод containsAll. В противном случае вы можете использовать количественные выражения и чистый метод contains. Если у вас нет таких чистых методов запросов, вам придется раскрывать детали реализации, например, базовое поле, что будет менее целесообразно для указания интерфейса.

Это прояснит проблему для вас?

...