데이빗 사양 : 촉진 및 작업을 하나 이상의 스키마

Question

을 적용 나는 Data 스키마의 순서를 추적 Array 스키마를 가지고있다. 프로모션을 사용하여 Array과 (과) 함께 사용할 수있는 Increment 작업을 승격 할 수 있습니다.

ArrayIncrement은 Array 안에 하나의 데이터 만 씩 증가시킵니다. 어떻게하면 마다Data을 \ran data 단위로 증가 시키나요?

Answer 1

모든 값을 증가하는 당신의 접근 방식의 기본 장애물은 (마지막 줄) 홍보의 관계형 재정의 사용이 지정하는 것입니다 그 위치 index?를 제외하고 data에서와 같은 값으로 data'지도의 모든 값. 이 무한 솔루션이있을 것없이, 우리는 도메인이 동일하게 유지 것을 주장 신체의 첫 번째 줄에서

--- ArrayIncrement --- 
| ΔArray 
--- 
| dom data = dom data' 
| ∀ i:dom data; ΔData · 
|  θData = data i ∧ θData' = data' i ∧ Increment 
------ 

:

한 가지 방법은 명시 적으로 모든 요소에 대한 관계를 통해 "반복"하는 것입니다 추가 요소.

다음 줄에서는 솔루션 색인 Promote의 두 번째 줄과 마찬가지로 특정 인덱스에서 전후 상태를 나타내는 변수를 설정합니다.