spec/containers/intrusive_doubly_linked_list/main.bend
bend-collections-laws-containers@1.0.0.0 · 71 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/model.bend as G
3import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/programs.bend as W
4
5# Contract of the intrusive doubly linked list (src/containers/
6# intrusive_doubly_linked_list.bend; contributed by Ryan Berckmans in
7# https://github.com/Giulio2002/bend-collections/pull/5).
8#
9# The model (model.bend) is a finite-map graph: every entity's next and prev
10# link, every root's head, and a frame P standing for everything else the
11# application owns. A list is valid when its members are unique, the root
12# reads the first member, and every member's links point at its neighbours
13# (a reciprocal, acyclic chain). programs.bend lists the exact field writes
14# each operation performs.
15#
16# The caller owns membership, so the SPARK preconditions below are real
17# obligations of the caller (SPARK's Pre): the list is valid, a prepended
18# entity is detached and not already a member, a removed entity is a member.
19# Under them, the clauses restate SPARK's Post for the model; the proof
20# package proves each one, and proves that the exported operations execute
21# the model's writes (for the ready-made table src/containers/
22# intrusive_links.bend: for every size).
23#
24# SPARK Formal_Doubly_Linked_Lists ours clauses
25# (SPARKlib spark-containers-formal-doubly_linked_lists.ads)
26# Prepend (Post: Model = new & old) prepend / prepend_as Prepend.valid, Prepend.other_roots, Prepend.frame
27# Delete (Post: Model = old minus remove Delete.first, Delete.inner, Delete.other_roots,
28# the element; P.Keys_Included) Delete.frame, Delete.detached
29# First (Post: head of the model) get_head First.head
30#
31# Not applicable: Append/Insert-after/Last/Length-by-count (no tail or count
32# in the root, by design), Element (payload stays in the application's
33# state), Clear/Copy/Move/Splice (the application owns node storage).
34
35# eq is a lawful identity test (~reflex) wherever the proof compares entities.
36
37# Prepend: a detached non-member n becomes the first member.
38def Prepend.valid(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +g: G.Graph<N,R,P>, +r: R, +n: N, +xs: List<&2,N>, +rsame: {req(r,r) == True{} : Bool}, +away: G.away(~N,~eq,n,xs), +detached: {G.prev(~N,~R,~P,~eq,g,n) == None{} : Maybe<&2,N>}, +valid: G.valid(~N,~R,~P,~eq,~req,g,r,xs)) -> Type:
39 G.valid(~N,~R,~P,~eq,~req,G.prepend(~N,~R,~P,~req,g,r,n),r,Con{n,xs})
40
41# Prepend: every other root reads what it read before.
42def Prepend.other_roots(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +x: R, +neq: {req(r,x) == False{} : Bool}) -> Type:
43 {G.head(~N,~R,~P,~req,G.prepend(~N,~R,~P,~req,g,r,n),x) == G.head(~N,~R,~P,~req,g,x) : Maybe<&2,N>}
44
45# Prepend: everything else the application owns is unchanged.
46def Prepend.frame(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N) -> Type:
47 {G.frame(~N,~R,~P,G.prepend(~N,~R,~P,~req,g,r,n)) == G.frame(~N,~R,~P,g) : P}
48
49# Delete the first member.
50def Delete.first(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +g: G.Graph<N,R,P>, +r: R, +n: N, +xs: List<&2,N>, +rsame: {req(r,r) == True{} : Bool}, +valid: G.valid(~N,~R,~P,~eq,~req,g,r,Con{n,xs})) -> Type:
51 G.valid(~N,~R,~P,~eq,~req,G.remove(~N,~R,~P,~eq,g,r,n),r,xs)
52
53# Delete a member after the prefix a ++ [p].
54def Delete.inner(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +g: G.Graph<N,R,P>, +r: R, +n: N, +a: List<&2,N>, +p: N, +b: List<&2,N>, +valid: G.valid(~N,~R,~P,~eq,~req,g,r,G.append(~N,G.append(~N,a,Con{p,Nil{}}),Con{n,b}))) -> Type:
55 G.valid(~N,~R,~P,~eq,~req,G.remove(~N,~R,~P,~eq,g,r,n),r,G.append(~N,G.append(~N,a,Con{p,Nil{}}),b))
56
57# Delete: every other root reads what it read before.
58def Delete.other_roots(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +x: R, +neq: {req(r,x) == False{} : Bool}) -> Type:
59 {G.head(~N,~R,~P,~req,G.remove(~N,~R,~P,~eq,g,r,n),x) == G.head(~N,~R,~P,~req,g,x) : Maybe<&2,N>}
60
61# Delete: everything else the application owns is unchanged.
62def Delete.frame(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N) -> Type:
63 {G.frame(~N,~R,~P,G.remove(~N,~R,~P,~eq,g,r,n)) == G.frame(~N,~R,~P,g) : P}
64
65# Delete: the removed entity no longer links forward (it can join another list).
66def Delete.detached(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +same: {eq(n,n) == True{} : Bool}) -> Type:
67 {G.next(~N,~R,~P,~eq,G.remove(~N,~R,~P,~eq,g,r,n),n) == None{} : Maybe<&2,N>}
68
69# First: a valid list's root reads its first member.
70def First.head(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +xs: List<&2,N>, +valid: G.valid(~N,~R,~P,~eq,~req,g,r,xs)) -> Type:
71 {G.head(~N,~R,~P,~req,g,r) == G.first(~N,xs,None{}) : Maybe<&2,N>}