A Denotational Semantics for Handel-C - Formal Methods and Hybrid Real-Time Systems - page 64

We have finite traces which correspond to zero or more iterations before the
condition becomes true, and one infinite trace which captures the situation were
b is always false —this is why we need to admit infinite traces in our semantic
model.

8 Conclusions and Future Work

We have presented a denotational semantics for Handel-C as sets of typed asser-
tion traces, which captures all the key behaviour of the language, with particular
emphasis on the proper treatment of default clauses in prialt statements. We
need to show that all this semantics describes the same language as does the op-
erational semantics. The real goal is to use the denotational semantics to verify a
series of algebraic laws for Handel-C, which would form the basis for a practical
system for formal reasoning about such programs. We also intended to extend
this to cover the notion of refinement in a Handel-C setting, linking the language
to specification notations such as CSP [35] or Circus [30].
Recently we have also published a “hardware semantics” for Handel-C [36],
which will allow us to explore transformations that investigate the trade-off
between the number of clock-cycles required to complete a task, and the length
of each cycle, which depends on the complexity of the combinatorial logic that
is generated. It is here that the well-known work of Zhou Chaochen on duration
calculus [37] and his work on modelling synchronous circuits at switch level [38]
will provide useful tools and insight for this work.
Finally, we hope to explore the embedding of these results into the UTP
framework [32], as a variant of Circus [30]. This work is being funded as a three-
year project by Science Foundation Ireland.

References

1. Celoxica Ltd.: Handel-C Language Reference Manual, v3.0. (2002),

www.celoxica.com
2. Hoare, C.A.R.: Communicating Sequential Processes. Intl. Series in Computer Sci-
ence. Prentice Hall, Englewood Cliffs (1985)
3. Page, I., Luk, W.: Compiling Occam into field-programmable gate arrays. In:
Moore, W., Luk, W. (eds.) FPGAs, Oxford Workshop on Field Programmable
Logic and Applications. Abingdon EE&CS Books, 15 Harcourt Way, Abingdon
OX14 1NV, UK, pp. 271-283 (1991)
4. Butterfield, A., Woodcock, J.: An operational semantics for handel-c. In: Arts,
T., Fokkink, W. (eds.) Electronic Notes in Theoretical Computer Science, vol. 80,
Elsevier, Amsterdam (2003)
5. Butterfield, A., Woodcock, J.: prialt in Handel-C: an operational semantics. Inter-
national Journal on Software Tool for Technology Transfer (STTT) (2005)
6. Butterfield, A.: Denotational semantics for prialt-free Handel-C. Technical Report
TCD-CS-2001-53, Dept. of Computer Science, Trinity College, Dublin University
(2001)