Module SimplifyPostConds

This module contains the implementation of the "postcondition" reducer which simplifies the postconditions in a list of function declarations w.r.t. a given list of theorems.

Note that theorems are standard (EasyCheck) properties having the prefix theorem', as

theorem'sortlength xs = length xs <~> length (sort xs)

theorem'sorted xs = always (sorted (sort xs))

Author: Michael Hanus

Version: August 2016

Summary of exported operations:

simplifyPostConditionsWithTheorems :: Int -> [CFuncDecl] -> [CFuncDecl] -> IO [CFuncDecl]

Exported operations:

simplifyPostConditionsWithTheorems :: Int -> [CFuncDecl] -> [CFuncDecl] -> IO [CFuncDecl]