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

== 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 ==