Created Date: 14/05/2024
Contributors: Wenwen Yan, Yingying Guo
Software: GNAT Community Edition 2019
Description: Given a uncompeleted package of Ada procedure for verifing the LZ77 decompression function, we are gonna finish the implementation of the depression and finish the SPARK verification of the correctness with the following the Hoear Logic(like assignment rule, consequence rule, sequencing rule, conditional rule and while rule).