南京大学：《程序设计语言的形式语义》课程教学资源（课件讲稿）Separation Logic（3/3）

Separation Logic (Ill) Acknowledgment:slides taken from Reynolds'mini-course CS 818A3

Separation Logic (III) Acknowledgment: slides taken from Reynolds’ mini-course CS 818A3

Notation for Sequences When a and B are sequences,we write .e for the empty sequence. [a]for the single-element sequence containing a.(We will omit the brackets when a is not a sequence.) a.3 for the composition of a followed by B. aT for the reflection of a. ●#a for the length of a. a;for the ith component of a

Notation for Sequences

Some Laws for Sequences aE=Q e·Q三Q ct=e [a]i [a] 共e=0 #[a]=1 a =eV 3a,a'.a [a]a (a:3)Y=a-(3.y) (aB)i =Bi.ai #(a:3)=（#a)+（#3) a=eV3a',a.a=a'.[a]

Some Laws for Sequences

Singly-linked Lists list ai: nil is defined by induction on the length of the sequence a(i.e.,by structural induction on a): list cid empi=nil list (a-a)i.,j list aj

Singly-linked Lists

Singly-linked List Segments lseg a (i,j): is defined by lseg e(i,j)der empij lseg a-a (i,k)aj sega(j,k)

Singly-linked List Segments

Singly-linked List Segments Properties lseg a(i,j)分i一a,j Iseg aB(i,k)j.Iseg a (i,j)*Iseg B(j,k) lseg a-b(i,k)÷j.Iseg a(i,j)*j→b,k list a i台Iseg a(i,nil)

Singly-linked List Segments

Emptyness Conditions For lists,one can derive a law that shows clearly when a list represents the empty sequence: list a i→(i=nil台a=e). For list segments,however,the situation is more complex.One can derive Iseg a(i,j)→(i=nil→(a=e∧j=nil)) Iseg a(i,j)→(i≠j→a卡e). But these formulas do not say whether a is empty when i =j nil

Emptyness Conditions

Nontouching List Segments When lseg a1·an(io,in), we have 3i1,.in-1: (i0一a1,i1)*(i1一a2,i2)*·*(in-1一an,in): Thus io,...,i1are distinct,but in is not constrained,and may equal any of the io,...,i1.In this case,we say that the list segment is touching. nontouching list segments {cycic{Cueiapingtortidoenbyy touching

Nontouching List Segments

Nontouching List Segments We can define nontouching list segments inductively by: ntlseg c(i,j)der empij ntlseg a-a (i,k)ik jntlseg a (j,k)) or equivalently,we can define them in terms of lseg: ntlseg a(,j）er Iseg a,DAj一 The obvious advantage of knowing that a list segment is non- touching is that it is easy to test whether it is empty: ntlseg a(i,j)→(a=e台i=j)

Nontouching List Segments

Nontouching List Segments Fortunately,there are common situations where list segments must be nontouching: list ai=ntlseg a(i,nil) Iseg a(i,j)*list Bj=ntlseg a (i,j)*list Bj lseg a(i,j)*j→-→ntlseg a(i,j)*j→-

Nontouching List Segments Fortunately, there are common situations where list segments must be nontouching: