copilot-language.github.io/about.html at master · Copilot-Language/copilot-language.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
<!DOCTYPE html>
<html>
    <head>
        <title>Copilot: about</title>
        <meta charset="utf-8">
        <link rel="stylesheet" href="style.css">
        <link rel="stylesheet" href="haskell.css">
    <body>
        <div id="page">
            <div id="header">
                <a href="index.html">Copilot</a>
                <span>Realtime Programming Language and Runtime Verification Framework</span>
            </div>
            <div id="menu"><p><a href="home.html">Home</a>
<a href="about.html">About</a>
<a href="download.html">Download</a>
<a href="documentation.html">Documentation</a>
<a href="contact.html">Contact</a>
<a href="https://github.com/copilot-language/copilot">Source Code</a></p></div>
            <div id="content">
                <h1>About</h1>

<p>Copilot is a realtime programming language and Runtime Verification framework.
It allows users to write concise programs in a simple but powerful way using a
stream-based approach.</p>

<p>Programs can be interpreted for testing, or translated C99 code to be
incorporated in a project, or as a standalone application. The C99 backend
ensures us that the output is constant in memory and time, making it suitable
for systems with hard realtime requirements. Copilot provides a strong type
system that helps keeping programmers from making common mistakes, aiding in
the quality of the code.</p>

<p>Copilot provides a library providing higher-level constructs, for example for
defining clocks, a Boyer-Moore majority voting implementation and various
temporal logics, including Linear Temporal logic (LTL) and Past Time LTL.</p>

<h2>Code example</h2>

<p>This is a simple example showing basic usage. It implements a home heating
system: It heats when temp gets too low, and stops when it is high enough.  It
reads temperature as a byte (range -50C to 100C) and translates this to
Celsius.</p>

<pre><code class="language-haskell"><mark class="comment">{-# LANGUAGE RebindableSyntax #-}</mark>

<mark class="keyword">module</mark> Main <mark class="keyword">where</mark>

<mark class="keyword">import</mark> Language.Copilot
<mark class="keyword">import</mark> Copilot.Compile.C99

<mark class="comment">-- External temperature as a byte, range of -50C to 100C.</mark>
temp :: Stream Word8
temp = extern <mark class="string">"temperature"</mark> Nothing

<mark class="comment">-- Calculate temperature in Celsius.
-- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there
-- is no direct relation between Word8 and Float.</mark>
ctemp :: Stream Float
ctemp = (unsafeCast temp) * (<mark class="literal">150.0</mark> / <mark class="literal">255.0</mark>) - <mark class="literal">50.0</mark>

spec = <mark class="keyword">do</mark>
  <mark class="comment">-- Triggers that fire when the ctemp is too low or too high,
  -- pass the current ctemp as an argument.</mark>
  trigger <mark class="string">"heaton"</mark>  (ctemp < <mark class="literal">18.0</mark>) [arg ctemp]
  trigger <mark class="string">"heatoff"</mark> (ctemp > <mark class="literal">21.0</mark>) [arg ctemp]

<mark class="comment">-- Compile the spec</mark>
main = reify spec >>= compile <mark class="string">"heater"</mark></code></pre>
            </div>
        </div>
    </body>
</html>