From 5a076109b09f4f684defcf1fca15170f2005e392 Mon Sep 17 00:00:00 2001
From: Cheunglo <12205569+Cheunglo@users.noreply.github.com>
Date: Fri, 3 Jan 2020 19:59:32 +1100
Subject: [PATCH] Added a descrption of files

---
 README.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/README.md b/README.md
index 51c166c..612667d 100644
--- a/README.md
+++ b/README.md
@@ -16,4 +16,9 @@ Word arrays are a commonly used data structure, especially in low level
 systems, so verifying these would be beneficial as this would reduce the
 overall cost of verification of any project that requires word arrays.
 
+The file WordArray.cogent contains the trivial Cogent program to generate the C implementations of the word array functions.
+The file WordArraySpec.thy contains the specification for word arrays.
+The file WordArrayT.thy contains the proofs of functional correctness and frame constraint satisfiability.
+The file main_pp_inferred.c is generated from the files main.ac and entrypoints.cfg from the make file Makefile. This file contains the C implementations of the word array functions.
+
 [![DOI](https://zenodo.org/badge/230601479.svg)](https://zenodo.org/badge/latestdoi/230601479)