Как читать дафны контрпримеры - PullRequest
Новая
       31

Как читать дафны контрпримеры

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

Я бы хотел понять контрпримеры, сделанные Дафни.В качестве примера я использую следующий код: 

function update_map<K(!new), V>(m1: map<K, V>, m2: map<K, V>): map<K, V>
ensures
  (forall k :: k in m1 || k in m2 ==> k in update_map(m1, m2)) &&
  (forall k :: k in m2 ==> update_map(m1, m2)[k] == m2[k]) &&
  (forall k :: !(k in m2) && k in m1 ==> update_map(m1, m2)[k] == m1[k]) &&
  (forall k :: !(k in m2) && !(k in m1) ==> !(k in update_map(m1, m2)))
{
  map k | k in (m1.Keys + m2.Keys) :: if k in m2 then m2[k] else m1[k]
}

predicate map_extends<K, V>(m1: map<K, V>, m2: map<K, V>) {
  forall k :: k in m2 ==> k in m1 && m1[k] == m2[k]
}

lemma update_map_extends<K, V>
  (m1: map<K, V>, m2: map<K, V>, m3: map<K, V>, m4: map<K, V>)
 requires map_extends(m1, m3)
 requires map_extends(m2, m4)
 requires m1.Keys !! m2.Keys
 ensures map_extends(update_map(m1, m2), update_map(m3, m4))
{}

lemma wrong_update_map_extends<K, V>
  (m1: map<K, V>, m2: map<K, V>, m3: map<K, V>, m4: map<K, V>)
 requires map_extends(m1, m3)
 requires map_extends(m2, m4)
 ensures map_extends(update_map(m1, m2), update_map(m3, m4))
{}

Моя первая попытка получить контрпример состояла в использовании кода Visual Studio с плагином functionalcorrectness.dafny-vscode, а затем включении опции dafny.automaticShowCounterModel.После этого мне иногда удается получить встроенный контрпример, нажав F7 или из меню, вызываемого правой кнопкой мыши, но иногда это не работает.Я пока не понимаю, когда эта функция работает, а когда нет, похоже, есть ошибка в пользовательском интерфейсе, но это не предмет этого вопроса.Контрпример, который он отображает, выглядит следующим образом: 

_module._default.wrong_update_map_extends$K -> T@U!val!58, _module._default.wrong_update_map_extends$V -> T@U!val!59, m1#0 -> T@U!val!60, m2#0 -> T@U!val!61, m3#0 -> T@U!val!62, m4#0 -> T@U!val!63

Итак, мой первый вопрос:

Как я могу интерпретировать этот контрпример?

Другая вещьЯ пытался запустить 

dafny -mv:updmodel.bvd update_map.dfy

и затем проверить файл updmodel.bvd, который гласит: 

*** MODEL
##_System._tuple#0._#Make0 -> T@U!val!39
##_System._tuple#2._#Make2 -> T@U!val!42
#_System._tuple#0._#Make0 -> T@U!val!55
$$Language$Dafny -> true
$_Frame -> **$_Frame
$_Frame@0 -> T@U!val!65
$_reverifyPost -> **$_reverifyPost
$FunctionContextHeight -> 3
$Heap@@5 -> T@U!val!57
$mv_state_const -> 13
$OneHeap -> T@U!val!50
$Tick -> **$Tick
%lbl%@1 -> false
%lbl%+0 -> true
%lbl%+2 -> true
_module._default.wrong_update_map_extends$K -> T@U!val!58
_module._default.wrong_update_map_extends$V -> T@U!val!59
alloc -> T@U!val!0
allocName -> T@U!val!24
boolType -> T@T!val!2
BoxType -> T@T!val!9
charType -> T@T!val!10
class._module.__default -> T@U!val!47
class._System.__tuple_h0 -> T@U!val!38
class._System.__tuple_h2 -> T@U!val!41
class._System.array? -> T@U!val!29
class._System.bool -> T@U!val!20
class._System.int -> T@U!val!19
class._System.multiset -> T@U!val!23
class._System.object? -> T@U!val!26
class._System.seq -> T@U!val!22
class._System.set -> T@U!val!21
ClassNameType -> T@T!val!6
DatatypeTypeType -> T@T!val!12
DtCtorIdType -> T@T!val!8
HandleTypeType -> T@T!val!14
intType -> T@T!val!0
k#5!867!125 -> T@U!val!66
LayerTypeType -> T@T!val!13
m1#0@@11 -> T@U!val!60
m2#0@@11 -> T@U!val!61
m3#0 -> T@U!val!62
m4#0 -> T@U!val!63
NameFamilyType -> T@T!val!7
NoTraitAtAll -> T@U!val!18
null -> T@U!val!52
realType -> T@T!val!1
refType -> T@T!val!11
rmodeType -> T@T!val!3
TagBool -> T@U!val!6
TagChar -> T@U!val!7
TagClass -> T@U!val!17
Tagclass._module.__default -> T@U!val!48
Tagclass._System.___hFunc0 -> T@U!val!32
Tagclass._System.___hFunc1 -> T@U!val!44
Tagclass._System.___hFunc2 -> T@U!val!35
Tagclass._System.___hPartialFunc0 -> T@U!val!33
Tagclass._System.___hPartialFunc1 -> T@U!val!45
Tagclass._System.___hPartialFunc2 -> T@U!val!36
Tagclass._System.___hTotalFunc0 -> T@U!val!34
Tagclass._System.___hTotalFunc1 -> T@U!val!46
Tagclass._System.___hTotalFunc2 -> T@U!val!37
Tagclass._System.__tuple_h0 -> T@U!val!40
Tagclass._System.__tuple_h2 -> T@U!val!43
Tagclass._System.array -> T@U!val!31
Tagclass._System.array? -> T@U!val!30
Tagclass._System.nat -> T@U!val!25
Tagclass._System.object -> T@U!val!28
Tagclass._System.object? -> T@U!val!27
TagIMap -> T@U!val!16
TagInt -> T@U!val!8
TagISet -> T@U!val!12
TagMap -> T@U!val!15
TagMultiSet -> T@U!val!13
TagORDINAL -> T@U!val!10
TagReal -> T@U!val!9
TagSeq -> T@U!val!14
TagSet -> T@U!val!11
TBool -> T@U!val!1
TChar -> T@U!val!2
Tclass._module.__default -> T@U!val!56
Tclass._System.__tuple_h0 -> T@U!val!54
Tclass._System.nat -> T@U!val!51
Tclass._System.object -> T@U!val!53
Tclass._System.object? -> T@U!val!49
TInt -> T@U!val!3
TORDINAL -> T@U!val!5
TReal -> T@U!val!4
TyTagType -> T@T!val!5
TyType -> T@T!val!4
unique-value!100 -> distinct-elems!74!val!24
unique-value!101 -> distinct-elems!74!val!25
unique-value!102 -> distinct-elems!74!val!26
unique-value!103 -> distinct-elems!74!val!27
unique-value!104 -> distinct-elems!74!val!28
unique-value!105 -> distinct-elems!74!val!29
unique-value!106 -> distinct-elems!74!val!30
unique-value!107 -> distinct-elems!74!val!31
unique-value!108 -> distinct-elems!74!val!32
unique-value!109 -> distinct-elems!74!val!33
unique-value!110 -> distinct-elems!74!val!34
unique-value!111 -> distinct-elems!74!val!35
unique-value!112 -> distinct-elems!74!val!36
unique-value!113 -> distinct-elems!74!val!37
unique-value!114 -> distinct-elems!74!val!38
unique-value!115 -> distinct-elems!74!val!39
unique-value!116 -> distinct-elems!74!val!40
unique-value!117 -> distinct-elems!74!val!41
unique-value!118 -> distinct-elems!74!val!42
unique-value!119 -> distinct-elems!74!val!43
unique-value!120 -> distinct-elems!74!val!44
unique-value!121 -> distinct-elems!74!val!45
unique-value!122 -> distinct-elems!74!val!46
unique-value!123 -> distinct-elems!74!val!47
unique-value!124 -> distinct-elems!74!val!48
unique-value!76 -> distinct-elems!74!val!0
unique-value!77 -> distinct-elems!74!val!1
unique-value!78 -> distinct-elems!74!val!2
unique-value!79 -> distinct-elems!74!val!3
unique-value!80 -> distinct-elems!74!val!4
unique-value!81 -> distinct-elems!74!val!5
unique-value!82 -> distinct-elems!74!val!6
unique-value!83 -> distinct-elems!74!val!7
unique-value!84 -> distinct-elems!74!val!8
unique-value!85 -> distinct-elems!74!val!9
unique-value!86 -> distinct-elems!74!val!10
unique-value!87 -> distinct-elems!74!val!11
unique-value!88 -> distinct-elems!74!val!12
unique-value!89 -> distinct-elems!74!val!13
unique-value!90 -> distinct-elems!74!val!14
unique-value!91 -> distinct-elems!74!val!15
unique-value!92 -> distinct-elems!74!val!16
unique-value!93 -> distinct-elems!74!val!17
unique-value!94 -> distinct-elems!74!val!18
unique-value!95 -> distinct-elems!74!val!19
unique-value!96 -> distinct-elems!74!val!20
unique-value!97 -> distinct-elems!74!val!21
unique-value!98 -> distinct-elems!74!val!22
unique-value!99 -> distinct-elems!74!val!23
$Is -> {
  T@U!val!55 T@U!val!54 -> true
  T@U!val!60 T@U!val!64 -> true
  T@U!val!61 T@U!val!64 -> true
  T@U!val!62 T@U!val!64 -> true
  T@U!val!63 T@U!val!64 -> true
  T@U!val!84 T@U!val!64 -> true
  T@U!val!85 T@U!val!64 -> true
  else -> true
}
$IsAlloc -> {
  T@U!val!60 T@U!val!64 T@U!val!57 -> true
  T@U!val!61 T@U!val!64 T@U!val!57 -> true
  T@U!val!62 T@U!val!64 T@U!val!57 -> true
  T@U!val!63 T@U!val!64 T@U!val!57 -> true
  else -> true
}
$IsAllocBox -> {
  T@U!val!66 T@U!val!58 T@U!val!57 -> true
  T@U!val!71 T@U!val!59 T@U!val!57 -> true
  T@U!val!73 T@U!val!59 T@U!val!57 -> true
  T@U!val!81 T@U!val!58 T@U!val!57 -> true
  T@U!val!82 T@U!val!59 T@U!val!57 -> true
  T@U!val!83 T@U!val!59 T@U!val!57 -> true
  else -> true
}
$IsBox -> {
  T@U!val!66 T@U!val!58 -> true
  T@U!val!71 T@U!val!59 -> true
  T@U!val!73 T@U!val!59 -> true
  T@U!val!81 T@U!val!58 -> true
  T@U!val!82 T@U!val!59 -> true
  T@U!val!83 T@U!val!59 -> true
  else -> true
}
$IsGhostField -> {
  T@U!val!0 -> false
  else -> false
}
$IsGoodHeap -> {
  T@U!val!50 -> true
  T@U!val!57 -> true
  else -> true
}
$IsHeapAnchor -> {
  T@U!val!57 -> true
  else -> true
}
$mv_state -> {
  13 0 -> true
  else -> true
}
[2] -> {
  T@U!val!67 T@U!val!66 -> true
  T@U!val!67 T@U!val!81 -> true
  T@U!val!69 T@U!val!66 -> true
  T@U!val!69 T@U!val!81 -> true
  T@U!val!70 T@U!val!66 -> T@U!val!71
  T@U!val!70 T@U!val!81 -> T@U!val!82
  T@U!val!72 T@U!val!66 -> T@U!val!73
  T@U!val!72 T@U!val!81 -> T@U!val!83
  T@U!val!74 T@U!val!66 -> T@U!val!73
  T@U!val!74 T@U!val!81 -> T@U!val!83
  T@U!val!75 T@U!val!66 -> T@U!val!73
  T@U!val!75 T@U!val!81 -> T@U!val!83
  T@U!val!76 T@U!val!66 -> true
  T@U!val!76 T@U!val!81 -> true
  T@U!val!77 T@U!val!66 -> true
  T@U!val!77 T@U!val!81 -> true
  T@U!val!78 T@U!val!66 -> T@U!val!71
  T@U!val!78 T@U!val!81 -> T@U!val!82
  T@U!val!79 T@U!val!66 -> true
  T@U!val!79 T@U!val!81 -> true
  T@U!val!80 T@U!val!66 -> false
  T@U!val!80 T@U!val!81 -> false
  else -> true
}
_module.__default.map__extends -> {
  T@U!val!58 T@U!val!59 T@U!val!60 T@U!val!62 -> true
  T@U!val!58 T@U!val!59 T@U!val!61 T@U!val!63 -> true
  T@U!val!58 T@U!val!59 T@U!val!84 T@U!val!85 -> false
  else -> true
}
_module.__default.map__extends#canCall -> {
  T@U!val!58 T@U!val!59 T@U!val!60 T@U!val!62 -> true
  T@U!val!58 T@U!val!59 T@U!val!61 T@U!val!63 -> true
  T@U!val!58 T@U!val!59 T@U!val!84 T@U!val!85 -> true
  else -> true
}
_module.__default.update__map -> {
  T@U!val!58 T@U!val!59 T@U!val!60 T@U!val!61 -> T@U!val!84
  T@U!val!58 T@U!val!59 T@U!val!62 T@U!val!63 -> T@U!val!85
  else -> T@U!val!84
}
bool_2_U -> {
  false -> false
  true -> true
  else -> true
}
Ctor -> {
  T@T!val!0 -> 0
  T@T!val!1 -> 1
  T@T!val!10 -> 11
  T@T!val!11 -> 17
  T@T!val!12 -> 18
  T@T!val!13 -> 19
  T@T!val!14 -> 20
  T@T!val!15 -> 7
  T@T!val!16 -> 16
  T@T!val!17 -> 23
  T@T!val!18 -> 14
  T@T!val!19 -> 12
  T@T!val!2 -> 2
  T@T!val!20 -> 12
  T@T!val!3 -> 3
  T@T!val!4 -> 4
  T@T!val!5 -> 5
  T@T!val!6 -> 6
  T@T!val!7 -> 8
  T@T!val!8 -> 9
  T@T!val!9 -> 10
  else -> 12
}
DatatypeCtorId -> {
  T@U!val!55 -> T@U!val!39
  else -> T@U!val!39
}
DeclName -> {
  T@U!val!0 -> T@U!val!24
  else -> T@U!val!24
}
distinct-aux-f!!75 -> {
  T@U!val!0 -> distinct-elems!74!val!23
  T@U!val!1 -> distinct-elems!74!val!0
  T@U!val!10 -> distinct-elems!74!val!9
  T@U!val!11 -> distinct-elems!74!val!10
  T@U!val!12 -> distinct-elems!74!val!11
  T@U!val!13 -> distinct-elems!74!val!12
  T@U!val!14 -> distinct-elems!74!val!13
  T@U!val!15 -> distinct-elems!74!val!14
  T@U!val!16 -> distinct-elems!74!val!15
  T@U!val!17 -> distinct-elems!74!val!16
  T@U!val!18 -> distinct-elems!74!val!17
  T@U!val!19 -> distinct-elems!74!val!18
  T@U!val!2 -> distinct-elems!74!val!1
  T@U!val!20 -> distinct-elems!74!val!19
  T@U!val!21 -> distinct-elems!74!val!20
  T@U!val!22 -> distinct-elems!74!val!21
  T@U!val!23 -> distinct-elems!74!val!22
  T@U!val!24 -> distinct-elems!74!val!24
  T@U!val!25 -> distinct-elems!74!val!25
  T@U!val!26 -> distinct-elems!74!val!26
  T@U!val!27 -> distinct-elems!74!val!27
  T@U!val!28 -> distinct-elems!74!val!28
  T@U!val!29 -> distinct-elems!74!val!29
  T@U!val!3 -> distinct-elems!74!val!2
  T@U!val!30 -> distinct-elems!74!val!30
  T@U!val!31 -> distinct-elems!74!val!31
  T@U!val!32 -> distinct-elems!74!val!32
  T@U!val!33 -> distinct-elems!74!val!33
  T@U!val!34 -> distinct-elems!74!val!34
  T@U!val!35 -> distinct-elems!74!val!35
  T@U!val!36 -> distinct-elems!74!val!36
  T@U!val!37 -> distinct-elems!74!val!37
  T@U!val!38 -> distinct-elems!74!val!38
  T@U!val!39 -> distinct-elems!74!val!39
  T@U!val!4 -> distinct-elems!74!val!3
  T@U!val!40 -> distinct-elems!74!val!40
  T@U!val!41 -> distinct-elems!74!val!41
  T@U!val!42 -> distinct-elems!74!val!42
  T@U!val!43 -> distinct-elems!74!val!43
  T@U!val!44 -> distinct-elems!74!val!44
  T@U!val!45 -> distinct-elems!74!val!45
  T@U!val!46 -> distinct-elems!74!val!46
  T@U!val!47 -> distinct-elems!74!val!47
  T@U!val!48 -> distinct-elems!74!val!48
  T@U!val!5 -> distinct-elems!74!val!4
  T@U!val!6 -> distinct-elems!74!val!5
  T@U!val!7 -> distinct-elems!74!val!6
  T@U!val!8 -> distinct-elems!74!val!7
  T@U!val!9 -> distinct-elems!74!val!8
  else -> distinct-elems!74!val!0
}
FDim -> {
  T@U!val!0 -> 0
  else -> 0
}
FieldType -> {
  T@T!val!2 -> T@T!val!15
  else -> T@T!val!15
}
FieldTypeInv0 -> {
  T@T!val!15 -> T@T!val!2
  else -> T@T!val!2
}
Inv0_TMap -> {
  T@U!val!64 -> T@U!val!58
  else -> T@U!val!58
}
Inv1_TMap -> {
  T@U!val!64 -> T@U!val!59
  else -> T@U!val!59
}
k#0@@1!838!72 -> {
  T@U!val!85 T@U!val!84 T@U!val!58 -> T@U!val!81
  else -> T@U!val!81
}
lambda#0 -> {
  T@U!val!61 T@U!val!58 T@U!val!60 -> T@U!val!69
  T@U!val!63 T@U!val!58 T@U!val!62 -> T@U!val!67
  else -> T@U!val!69
}
lambda#1 -> {
  T@U!val!61 T@U!val!60 -> T@U!val!70
  T@U!val!63 T@U!val!62 -> T@U!val!72
  else -> T@U!val!70
}
lambda#9 -> {
  T@U!val!0 T@U!val!52 T@U!val!57 -> T@U!val!65
  else -> T@U!val!65
}
Lit -> {
  T@U!val!55 -> T@U!val!55
  else -> T@U!val!55
}
Map#Domain -> {
  T@U!val!60 -> T@U!val!76
  T@U!val!61 -> T@U!val!79
  T@U!val!62 -> T@U!val!77
  T@U!val!63 -> T@U!val!80
  T@U!val!84 -> T@U!val!69
  T@U!val!85 -> T@U!val!67
  else -> T@U!val!67
}
Map#Elements -> {
  T@U!val!60 -> T@U!val!75
  T@U!val!61 -> T@U!val!78
  T@U!val!62 -> T@U!val!74
  T@U!val!84 -> T@U!val!70
  T@U!val!85 -> T@U!val!72
  else -> T@U!val!70
}
Map#Glue -> {
  T@U!val!67 T@U!val!72 T@U!val!64 -> T@U!val!85
  T@U!val!69 T@U!val!70 T@U!val!64 -> T@U!val!84
  else -> T@U!val!84
}
MapType -> {
  T@T!val!9 T@T!val!9 -> T@T!val!18
  else -> T@T!val!18
}
MapType0Type -> {
  T@T!val!9 T@T!val!2 -> T@T!val!20
  T@T!val!9 T@T!val!9 -> T@T!val!19
  else -> T@T!val!19
}
MapType0TypeInv0 -> {
  T@T!val!19 -> T@T!val!9
  T@T!val!20 -> T@T!val!9
  else -> T@T!val!9
}
MapType0TypeInv1 -> {
  T@T!val!19 -> T@T!val!9
  T@T!val!20 -> T@T!val!2
  else -> T@T!val!9
}
MapType1Type -> {
  T@T!val!11 -> T@T!val!16
  else -> T@T!val!16
}
MapType1TypeInv0 -> {
  T@T!val!16 -> T@T!val!11
  else -> T@T!val!11
}
MapType4Type -> {
  T@T!val!11 T@T!val!2 -> T@T!val!17
  else -> T@T!val!17
}
MapType4TypeInv0 -> {
  T@T!val!17 -> T@T!val!11
  else -> T@T!val!11
}
MapType4TypeInv1 -> {
  T@T!val!17 -> T@T!val!2
  else -> T@T!val!2
}
MapTypeInv0 -> {
  T@T!val!18 -> T@T!val!9
  else -> T@T!val!9
}
MapTypeInv1 -> {
  T@T!val!18 -> T@T!val!9
  else -> T@T!val!9
}
Tag -> {
  T@U!val!1 -> T@U!val!6
  T@U!val!2 -> T@U!val!7
  T@U!val!3 -> T@U!val!8
  T@U!val!4 -> T@U!val!9
  T@U!val!49 -> T@U!val!27
  T@U!val!5 -> T@U!val!10
  T@U!val!51 -> T@U!val!25
  T@U!val!53 -> T@U!val!28
  T@U!val!54 -> T@U!val!40
  T@U!val!56 -> T@U!val!48
  T@U!val!64 -> T@U!val!15
  else -> T@U!val!6
}
tickleBool -> {
  false -> true
  true -> true
  else -> true
}
TMap -> {
  T@U!val!58 T@U!val!59 -> T@U!val!64
  else -> T@U!val!64
}
type -> {
  false -> T@T!val!2
  T@U!val!0 -> T@T!val!15
  T@U!val!1 -> T@T!val!4
  T@U!val!10 -> T@T!val!5
  T@U!val!11 -> T@T!val!5
  T@U!val!12 -> T@T!val!5
  T@U!val!13 -> T@T!val!5
  T@U!val!14 -> T@T!val!5
  T@U!val!15 -> T@T!val!5
  T@U!val!16 -> T@T!val!5
  T@U!val!17 -> T@T!val!5
  T@U!val!18 -> T@T!val!6
  T@U!val!19 -> T@T!val!6
  T@U!val!2 -> T@T!val!4
  T@U!val!20 -> T@T!val!6
  T@U!val!21 -> T@T!val!6
  T@U!val!22 -> T@T!val!6
  T@U!val!23 -> T@T!val!6
  T@U!val!24 -> T@T!val!7
  T@U!val!25 -> T@T!val!5
  T@U!val!26 -> T@T!val!6
  T@U!val!27 -> T@T!val!5
  T@U!val!28 -> T@T!val!5
  T@U!val!29 -> T@T!val!6
  T@U!val!3 -> T@T!val!4
  T@U!val!30 -> T@T!val!5
  T@U!val!31 -> T@T!val!5
  T@U!val!32 -> T@T!val!5
  T@U!val!33 -> T@T!val!5
  T@U!val!34 -> T@T!val!5
  T@U!val!35 -> T@T!val!5
  T@U!val!36 -> T@T!val!5
  T@U!val!37 -> T@T!val!5
  T@U!val!38 -> T@T!val!6
  T@U!val!39 -> T@T!val!8
  T@U!val!4 -> T@T!val!4
  T@U!val!40 -> T@T!val!5
  T@U!val!41 -> T@T!val!6
  T@U!val!42 -> T@T!val!8
  T@U!val!43 -> T@T!val!5
  T@U!val!44 -> T@T!val!5
  T@U!val!45 -> T@T!val!5
  T@U!val!46 -> T@T!val!5
  T@U!val!47 -> T@T!val!6
  T@U!val!48 -> T@T!val!5
  T@U!val!49 -> T@T!val!4
  T@U!val!5 -> T@T!val!4
  T@U!val!50 -> T@T!val!16
  T@U!val!51 -> T@T!val!4
  T@U!val!52 -> T@T!val!11
  T@U!val!53 -> T@T!val!4
  T@U!val!54 -> T@T!val!4
  T@U!val!55 -> T@T!val!12
  T@U!val!56 -> T@T!val!4
  T@U!val!57 -> T@T!val!16
  T@U!val!58 -> T@T!val!4
  T@U!val!59 -> T@T!val!4
  T@U!val!6 -> T@T!val!5
  T@U!val!60 -> T@T!val!18
  T@U!val!61 -> T@T!val!18
  T@U!val!62 -> T@T!val!18
  T@U!val!63 -> T@T!val!18
  T@U!val!64 -> T@T!val!4
  T@U!val!65 -> T@T!val!17
  T@U!val!66 -> T@T!val!9
  T@U!val!67 -> T@T!val!20
  T@U!val!69 -> T@T!val!20
  T@U!val!7 -> T@T!val!5
  T@U!val!70 -> T@T!val!19
  T@U!val!71 -> T@T!val!9
  T@U!val!72 -> T@T!val!19
  T@U!val!73 -> T@T!val!9
  T@U!val!74 -> T@T!val!19
  T@U!val!75 -> T@T!val!19
  T@U!val!76 -> T@T!val!20
  T@U!val!77 -> T@T!val!20
  T@U!val!78 -> T@T!val!19
  T@U!val!79 -> T@T!val!20
  T@U!val!8 -> T@T!val!5
  T@U!val!80 -> T@T!val!20
  T@U!val!81 -> T@T!val!9
  T@U!val!82 -> T@T!val!9
  T@U!val!83 -> T@T!val!9
  T@U!val!84 -> T@T!val!18
  T@U!val!85 -> T@T!val!18
  T@U!val!9 -> T@T!val!5
  true -> T@T!val!2
  else -> T@T!val!5
}
U_2_bool -> {
  false -> false
  true -> true
  else -> true
}
*** STATE <initial>
  $_Frame -> **$_Frame
  $_reverifyPost -> **$_reverifyPost
  $Heap -> T@U!val!57
  $Tick -> **$Tick
  _module._default.wrong_update_map_extends$K -> T@U!val!58
  _module._default.wrong_update_map_extends$V -> T@U!val!59
  m1#0 -> T@U!val!60
  m2#0 -> T@U!val!61
  m3#0 -> T@U!val!62
  m4#0 -> T@U!val!63
*** END_STATE
*** STATE update_map.dfy(28,0): initial state
  $_Frame -> T@U!val!65
*** END_STATE
*** END_MODEL

Это, кажется, более подробно, но я все еще не понимаюкак это интерпретировать, поэтому мой второй вопрос:

Как я могу интерпретировать такие bvd-файлы?

Затем я прочитал об отладчике верификации Boogie, поэтому я клонировал ипостроил https://github.com/boogie-org/boogie/tree/cd0609f660a5f063b10eacdae142c915115ec162, и запустил BVD с файлом модели, созданным выше, и он произвел следующее:

BVD Screenshot

Мой третий вопрос:

Это выглядит как ожидалось?Если да, как это интерпретировать?

1 Ответ

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

Это не очень хороший ответ, но я все равно публикую его как ответ, а не комментарий, потому что считаю, что это состояние дел.

Насколько я знаю, никто, кто использует Дафнисмотрит на контрпримеры.(Могут быть некоторые люди, которые используют Boogie через другие внешние интерфейсы, которые смотрят на контрпримеры.) Лично я никогда даже не пытался взглянуть на контрпримеры.Вместо этого, когда я получаю ошибку проверки, я пытаюсь добавить утверждения в свою программу, чтобы выяснить, в чем проблема.Вы можете думать о assert P как о том, что задаете проверяющему вопрос «знаете ли вы, что P истинно?».Тогда вы можете использовать это, чтобы сузить вашу проблему.

...