Extended static checking for haskell

摘要: Program errors are hard to detect and costly both programmers who spend significant efforts in debugging, systems that guarded by runtime checks. Extended static checking can reduce these costs helping bugs at compile-time, where possible. has been applied objectoriented languages, like Java C#, but it not a lazy functional language, Haskell. In this paper, we describe an extended tool for Haskell, named ESC/Haskell, is based on symbolic computation assisted few novel strategies. One novelty our use of Haskell as the specification language itself pre/post conditions. Any function (including recursive higher order functions) be used which allows sophisticated properties expressed. To perform automatic verification, rely technique augmented counter-example guided unrolling. This automate verification process efficiently implemented.