Graveyard's correctness :

Graveyard is based on the Operational Transformation approach. In this approach, the correctness is ensured by the verification of some properties. To verify that the transformation functions ensure these properties, the automatic theorem prover Spike can be used.

The transformation functions used in graveyard have been specified in Spike langage. The proof can be performed using the following command: spike_nc.exe Compensation.spike for windows or ./spike_nc Compensation.spike for linux

Specification files
  • undo: specification file for actually implemented transformation functions.