The copilot package

Can you write a list in Haskell? Then you can write embedded C code using Copilot. Here's a Copilot program that computes the Fibonacci sequence (over Word 64s) and tests for even numbers:

 fib :: Streams
 fib = do
  let f = varW64 "fib"
  let t = varB "t"
  f .= [0,1] ++ f + (drop 1 f)
  t .= even f
    where even :: Spaec Word64 -> Spec Bool
          even w' = w' `mod` 2 == 0

Copilot contains an interpreter, a compiler, and uses a model-checker to check the correctness of your program. The compiler generates constant time and constant space C code via Tom Hawkin's Atom (thanks Tom!). Copilot was originally developed to write embedded monitors for more complex embedded systems, but it can be used to develop a variety of functional-style embedded code.

Properties

Versions	0.21, 0.22, 0.23, 0.25, 0.26, 0.27, 0.28, 1.0, 1.0.1, 1.0.2, 2.0, 2.0.1, 2.0.2, 2.0.3, 2.0.4, 2.0.5, 2.0.6, 2.0.7, 2.0.8, 2.0.9, 2.1.0, 2.1.1
Dependencies	atom (≥1.0.7), base (>4 & <6), containers (≥0.2.0.1), directory (≥1.0.0.0), filepath (≥1.0.0.0), mtl (≥1.0.0.0), process (≥1.0.0.0), random (≥1.0.0.0)
License	BSD3
Author	Lee Pike, Robin Morisset, Alwyn Goodloe, Sebastian Niller
Maintainer	Lee Pike <leepike@galois.com>
Category	Language
Home page	http://leepike.github.com/Copilot/
Upload date	Sat Nov 13 00:20:02 UTC 2010
Uploaded by	LeePike
Built on	ghc-6.12

Modules

Downloads

copilot-0.26.tar.gz (Cabal source package)
package description (included in the package)