How will one mark up a C program for the TASS model extractor? This page is organized by issues that arise.

Some of these problems might be solved by having the user assume there is an identifier _TASS. Then the user can use #ifdef blocks to wrap statements used by TASS but not a standard C compiler.

Input/Output

A real scientific program written in C does not have "input" and "output" variables Inputs may come from a variety of sources, mainly from files. But preprocessor directives may also be considered input, there may be input from the terminal, or from other sources. Output is also typically written to files or the screen. How do we model the input/output in this case? What should we expect the user to do? Perhaps the user should write a "TASS harness" which wraps the code in some way that specifies the input and output clearly? Ideas, please.

Assumptions

In MiniMP one writes:

input int N {N>0};

How to do this in C?

Non-deterministic select statement

Does not exist in C. Do we need it?

Assertion Language

Some MiniMP expressions do not occur in C, such as forall, exists. For accuracy, there is also the derivative notation. How to express them? Where can they occur? Can we use C's assert?

Loop invariants/co-invariants

Library calls

Think of the functions in stdlib, stdio, etc. We need some sort of abstract model of at least the most commonly-used functions. Most of them do not have state and should be representable in a simple way, perhaps abstracted away altogether.

Abstract Functions