-
Exported names:
-
Imported modules:
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: March 2021
Summary of exported operations:
simplifyPostConditionsWithTheorems
:: Int -> [CFuncDecl] -> [CFuncDecl] -> IO [CFuncDecl] 
|
Exported operations:
|
|