Code covered by the BSD License  

Highlights from
Tabular Expression Toolbox

image thumbnail

Tabular Expression Toolbox

by

 

23 Sep 2010 (Updated )

A tool for creating tabular expressions in Matlab/Simulink integrating checking with PVS and CVC3.

Working with floating point numbers

Working with floating point numbers

Contents

Floating point numbers

One of the limitations with computers is the way that we have to represent real numbers. In a theoretical sense the real numbers has infinite range and infinite precision, however when we want to represent these numbers in a machine using the standard numerical representation for a variety of reasons we lose these properties.

Matlab and most computers use the IEEE 754 floating point standard. The standard defines the way real numbers can be represented from the bit level including the results of operations, and exceptions.

A full discussion of the standard is beyond the scope of this document we refer the interested reader to Matlab's documentation as well as the standard documentation

Proving tables with floating point numbers

The toolbox has support for proving tables with floating point inputs. Currently only PVS is supported for this feature, and in general manual intervention with the prover will likely be required.

Several new types are provided which can be used as anyother type in the input and output fields.

  • single - a finite or infinite single precision number
  • single_finite - a finite single precision number
  • double - a finite or infinite double precision number
  • double_finite - a finite double precision number

A sample input string might be "x:double_finite, y:double_finite". The same rules for subtyping still apply, as it may be necessary to subtype inputs in order to get them to typecheck properly.

Contact us