I can imagine a huge number of properties.

1. Eventual consistency: if no new edits are generated, then eventually all connected viewers see the same document.

2. Durability: if the system acknowledges an edit, then that edit is stored permanently in the undo/redo chain of a document.

3. Causal consistency: if the system acknowledges an edit B that depends (for some definition of depend) on edit A, then it must have acknowledged A (instead of e.g. throwing away A due to a conflict and then acknowledging B).

4. Eventual connection: if, after a certain point, the user never fails any part of the handshake process, eventually the user can successfully connect to the document (there are definitely bugs in collaborative tools where users end up never able to connect to a document even with no problems in the connection)

5. Connection is idempotent: Connecting once vs connecting n times has the same result (ensuring e.g. that the process of connecting doesn't corrupt the document)

6. Security properties hold: any user who doesn't have the permissions to view a document is always denied access to the document (because there are sometimes security bugs where an unforeseen set of steps can actually lead to viewing the doc)

6. Order preservation of edits: for any user, even a user with intermittent connection problems, the document they see always has an ordered subset of the edits that user has made (i.e. the user never sees their edits applied out of order)

7. Data structure invariants hold: these documents are ultimately backed by data structures, sometimes complex ones that require certain balancing properties to be true. Make sure that those hold under all edits of the document.

Etc. There's probably dozens of properties at least you could write and check even for an abstract Google Doc-like system (to say nothing of the particulars of a specific implementation). That's not to say you have to write or verify all of these properties! Even just choosing one or two can give a huge boost in reliability confidence.

▲

ngruhn 5 days ago | parent [-]

Thanks that's very helpful. That all requires that you model both server and client together, right? You can't just treat "connection established" as a nondeterministic event that just "happens" to the client at some point.

▲

dwohnitmok 5 days ago | parent [-]

No you can also model things that are client-only or server-only using such non-deterministic events.

For example you could have the following client-only properties where you can treat "connection established" as an entirely non-deterministic event that randomly just pops in and happens to the client.

1. Every edit that is stored on the client is preserved in the client's undo/redo log (e.g. a remote edit after a connection established can't clobber any client's local edits that are already preserved in history)

2. Document invariants always hold no matter what connection established/remote edits come in (e.g. even if the document shrinks as a result of remote deletions, the cursor is always in a valid location)

3. Causal consistency and order preservation can be rescoped to also be client-only properties

4. Undoing and redoing with no other local edits always returns back to the original state (e.g. making sure that remote edits coming in don't violate user's expectations about how to get back to a known state) for some definition of "original state" (this depends a lot on how you want to handle merging of remote edits)

5. Remote edits are always applied after a multi-component edit not in the middle (e.g. we never apply a remote edit in the middle of a grapheme cluster such as an emoji or when we're in the middle of writing one).

6. We handle connection affinity properly (e.g. we might have multiple servers for redundancy that can all be connected to, but over the course of a session we cache data for a single endpoint to improve performance that will need to be recalculated if we connect to a new endpoint), so checking that the initial connection to a new endpoint from the client always has the data that the new endpoint needs and we're able to re-establish the connection that doesn't corrupt our client's local data etc.

Etc.

	▲	ngruhn 3 days ago \| parent [-]
		Very helpful. Thank you!