Examples

This page contains examples of BlockLibrary specification.

Textual specification examples

Following examples have been created using the BlockLibrary Textual Editor (see Textual editor) and show the concrete syntax of BlockLibrary specifications.

These files can be used as input to other BlockLibrary tools. E.g. Why code generation and verification in the Why toolset.

  • Some simple blocks – SimpleBlocks.bls.
    • Constant
    • Abs
    • Saturate
    • MinMax
    • MultiPortSwitch
    • RelationalOperator
    • Logic
    • Switch
    • Lookup
    • UnitDelay
  • Highly polymorphic blocks

In the following, we will provide an overview of the elements generated from a BlockLibrary specification model. Detailed informations, specification and verification results can be found on the BlockLibrary specification page.

Block variation graph

The BlockLibrary toolset allows to generate a block variation graph based on a block type specification to graphically display the structure of the specification. Here are some examples:

../_images/Abs.png ../_images/Sum.png

Why code generation

You can use the BlockLibrary toolset (See Eclipse update site) to generate Why modules and theories from block type specifications and perform additional formal verification of the specification with the Why toolset and the theorem provers that are available through it.

For example, from Abs block a following Why module SimpleBlocks_Abs.why and theories SimpleBlocks_Abs_compute.mlw are generated.

Video demonstration

Some video demonstrations are available for the toolset:

  • Demo.mp4 gives a general demonstration of the editor and verification tools.
  • Demo_Error.mp4 gives a demonstration of the proof debugging during verification with why3ide tool.

NOTE! The BlockLibrary DSL and tools are still under development. It is possible that some of the examples or features are slightly out of date. In case of problems you are welcome to send us a question or a bug report!

Table Of Contents

Previous topic

Testing and Simulation

Next topic

Eclipse update site

This Page