1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
For simplicity, allow typestates on enums, booleans and optional types only?
type T = private [typestate state (Uninitialized, Connected, Closed)]
type T = (
# storing the typestate here is optional, unless there are functions that have typestates in "when" clauses
enum (Uninitialized, Connected, Closed) state
int socket [state in Connected]
int bytes_written [state in Connected,Closed]
)
func create_socket()
returns rwref takeown T [return.state to Uninitialied]
func connect(rwref T this, ref SockAddr addr, int port)
returns |neterror.noroute [T.state from Uninitialized, when success(return) T.state to Connected]
---
alt. syntax:
func create_socket()
returns rwref takeown T
typestate return.state to Uninitialied
func connect(rwref T this, ref SockAddr addr, int port)
returns |neterror.noroute
typestate T.state from Uninitialized
typestate T.state to Connected when success(return)
# ^ if there is only one typestate it should be enough to say "typestate T to/from ..."
# example of wildcard typestate usage
func connect(rwref T this, ref SockAddr addr, int port)
returns |neterror.noroute
typestate T.state to Connected when T.state from Uninitialized and success(return)
---
alt syntax 2:
func create_socket()
returns rwref takeown T
postcond typestate return.state == Uninitialied
func connect(rwref T this, ref SockAddr addr, int port)
returns |neterror.noroute
precond typestate T.state == Uninitialized
postcond typestate T.state == Connected when success(return)
# ^ if there is only one typestate it should be enough to say "typestate T to/from ..."
# example of wildcard typestate usage
func connect(rwref T this, ref SockAddr addr, int port)
returns |neterror.noroute
typestate T.state to Connected when T.state from Uninitialized and success(return)
|
