Skip to content

Translating a subset of ABS to pure Haskell for proving correctness and resource consumption

License

Notifications You must be signed in to change notification settings

abstools/abs-haskell-formal

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

18 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Formal translation of ABS-subset to Haskell

Build Status License (3-Clause BSD) online API docs

A library to write (embed) ABS-subset programs in Haskell, and execute them at runtime by an included Haskell interpreter.

Prerequisites

You need a fairly-recent GHC compiler or Haskell Platform

Installing this library

Run inside the repository directory:

cabal install

Running the bechmarks

The ABS-subset benchmarks are under benchmarks/ directory, embedded as Haskell. After installing this library, you can compile them with:

ghc --make benchmarks/<FOLDER>/progs/ExampleName.hs

Execute an example with:

./benchmarks/<FOLDER>/progs/ExampleName

which will output the number of steps executed, the final heap, and the heap counter, e.g.:

Real steps:	6
Total steps:	6
Object Heap with array-size:10{
(0,([(0,-123),(1,8),(2,1),(3,9),(4,1)],fromList []))
}
Future Heap with array-size:10{
(1,Right (-123))
}
Counter: 2

Building the API docs

Run inside the repository directory:

cabal configure
cabal haddock

The documentation will appear under dist/doc/html

About

Translating a subset of ABS to pure Haskell for proving correctness and resource consumption

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published