@ Hovercouch의 답변에 추가 : "삭제"는 프로그래밍 언어와 달리 TLA + 사양의 의미와 일치하지 않습니다. VARIABLE 같은 dictionary 선언
것도 될 수있다. [1, 초. 6.5, p.72, Sec. "하지 마라."(p.80, pp.139-140). 실제로 dictionary이 값 "foo"에 값 "foo" 매핑하기 때문에 이러한 상태에서 상태 술어
dictionary["foo"] = "foo"
의 값은 TRUE입니다. 반대로, 상태 술어 :
dictionary["foo"] = "bar"
"foo" # "bar" 때문에 FALSE이다. 첫 번째로 그 상태와 단계에서, 우리는 쓰기 ([1, P.82]도 참조)
(dictionary["foo"] = "foo")'
을 우리가 표현 dictionary["foo"]이 다음 상태에서 "foo"에 해당 것만 말하고있다. 우리는 dictionary이 그 상태에있는 함수라고 말하지 않았습니다. 단지 dictionary["foo"]이 "foo"과 같아지는 값입니다. 어쩌면 dictionary은 그곳의 기능이 아닙니다.
기능이란 무엇입니까?
언제 주어진 값 f을 "함수"라고 부릅니까? 그 f 운영자 IsAFunction가 [1, p.303]로 정의되는 화학식 IsAFunction(f) 만족 일어나는 경우 대답은 :
IsAFunction(g) == g = [x \in DOMAIN g |-> g[x]]
튜플 ("배열")는 일부 n \in Nat위한 도메인 1..n과 기능은. TLA +에서 함수는 단순히 위 속성을 갖는 값입니다.ZF의 모든 값은 집합이므로, 함수는 집합이며, f이 [1, 위의 초] 함수 인 경우에도 y \in f을 쓸 수 있습니다. 4.5 절, p.33 절, 3.3 절 p30 절]. 우리가 모르기 때문에
---- MODULE test ----
EXTENDS TLAPS
f == [x \in {} |-> x]
g == [x \in {1, 2} |-> 3]
THEOREM
LET
S == f \cup {g}
IN
(1 \in f) => (1 \in S)
PROOF BY Zenon
(* you can replace this with OBVIOUS *)
=====================
(모델 검사기 TLC이 열거 상태를, 그리고 :
예를 들어, 정리의 증명 TLAPS으로 우리는 다음과 같은 정리를 증명할 수 tlapm -v -C test.tla을 실행하여 Isabelle를 사용하여 증거를 확인 어떤 요소가 한 세트의 함수로 포함되어있는 경우, TLC는 표현식 y \in f을 평가할 수 없으며 Error: Attempted to check if the value: ... is an element of the function ...을 발생시킬 수 있습니다. 구문 분석기 SANY은 위 모듈의 형식이 올바른지 확인합니다.
f이 함수가 아니거나 x \notin DOMAIN f 일 때 f[x]이라고 쓸 수도 있습니다. 문제는 그러한 경우에 f[x]의 값이 지정되지 않았으므로 사양은 값이 무엇인지에 따라 달라져서는 안됩니다. 사양
표현 dictionary = []에
댓글은 TLA +의 일부가 아닙니다. 이 의도되어 있기 때문에,
dictionary = [x \in {} |-> TRUE]
가 나는 CONSTANT으로 capacity를 선언합니다 : 빈 도메인과 기능을 쓰려면 (정확히 하나의 기능이있는 것은, 기능 extensionality [1, p.303]에 대한 공리 참조) (물론 변경되지 않는 한) 행동에 대해 변함없이 유지됩니다. 또한 currentSize은 사양에 따라 감소하지 않지만 아직 추가되지 않았다고 가정합니다.
또한 dictionary은 각 항목을 고유 한 값으로 매핑하지만 queue은 동일한 항목의 여러 복사본을 포함 할 수 있습니다. OP가이 사건을 위해 의도하는 것이 확실하지 않습니다.
EXTENDS Integers, Sequences
CONSTANT capacity
VARIABLES currentSize, queue, dictionary
Init == /\ (capacity = 3) /\ (currentSize = 0)
/\ (queue = <<>>) /\ (dictionary = [x \in {} |-> TRUE])
AddItem(Item, Value) ==
IF currentSize < capacity
(* Overwrite to what value the dictionary maps
the value. *)
THEN /\ currentSize' = currentSize + 1
/\ queue' = Append(queue, Item)
/\ dictionary' =
[x \in DOMAIN dictionary |->
IF x = Item
THEN Value
ELSE dictionary[x]]
(* Remove the leading item from the dictionary's domain,
then add the given item (perhaps the same), and
map it to the given value. *)
ELSE /\ queue' = Append(Tail(queue), Item)
/\ LET
(* It can happen that OldDom = NewDom. *)
OldDom == DOMAIN queue
first == queue[1]
TailDom == OldDom \ { first }
NewDom == TailDom \cup {Item}
IN
dictionary' =
[x \in NewDom |->
IF x = Item
THEN Value
ELSE dictionary[x]]
GetItem(Item) == dictionary[item]
Next == \/ AddItem
\/ GetItem
dictionary' = [x \in DOMAIN dictionary |->
IF x = Item THEN Value ELSE dictionary[x]]
식 [1, P.49]
dictionary' = [dictionary EXCEPT ![Item] = Value]
가 dictionary' = [x \in NewDom |->
IF x = Item THEN Value ELSE dictionary[x]]
가 EXCEPT로 대체 할 수없는 식으로 대체 될 수있다.
참조
[1] 레슬리 램 포트, "Specifying systems", 애디슨 - 웨슬리 2002
가이드는 여기에 문제를 제기,이 구조를 설명하는 방법에 오해의 소지가있다 : https://github.com/hwayne/ learntla/issues/41 – Hovercouch