Submission #6

The activity described and discussed at the present report is a continuation of initial preparations for DePool provided described in the ​Phase-1 specification document (see Submission 2). While Phase-1 was concentrated on descriptions in the form of natural language and different kinds of diagrams the most important part of the current Phase-2 is a code written in Coq language while the present report limits its value to supporting documentation.

The main goal of Phase-2 is to prepare the specification in the form of the formal computer language (such as Coq) as well as to provide proofs at functional level leaving all the cross-functional (business) level proofs to Phase-3.

The present report describes and discusses the complete workflow of the Phase-2 providing code examples as illustrations, however it’s just an auxiliary part of the Phase-2 keeping the codebase​provided as the main part of the delivery.



Links and attachments


Follow the link below to see statistical information about this submission.