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