Changes between Version 13 and Version 14 of C Interface
- Timestamp:
- 06/04/10 12:09:03 (16 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
C Interface
v13 v14 3 3 == Input/Output == 4 4 5 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.5 Question: 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. 6 6 7 I/O to/from files (including stdout) will be handled by creating an abstract model of the stdio library. This will introduce some shared variables (for the files) and define functions corresponding to the usual ones in stdio.h. There will be no need for user annotations, except for exceptional situations (e.g., to ignore a certain input or output command). Further details are coming.7 Answer: I/O to/from files (including stdout) will be handled by creating an abstract model of the stdio library. This will introduce some shared variables (for the files) and define functions corresponding to the usual ones in stdio.h. There will be no need for user annotations, except for exceptional situations (e.g., to ignore a certain input or output command). Further details are coming. 8 8 9 9 The argv and argc parameters passed to main will become the input variables for the model. There are some ways pre-processor object-type macros can also be treated as inputs, but some thought will have to be put into this. … … 12 12 == Assumptions == 13 13 14 In MiniMP one writes:14 Question: In MiniMP one writes: 15 15 {{{ 16 16 input int N {N>0}; … … 26 26 == Non-deterministic select statement == 27 27 28 Does not exist in C. Do we need it?28 Question: Does not exist in C. Do we need it? 29 29 30 30 == Assertion Language == 31 31 32 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}}}?32 Question: 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}}}? 33 33 34 34 Answer: probably we cannot use C's assert for expressions which are not C expressions. Instead use pragmas: … … 41 41 == Loop (joint) invariants == 42 42 43 These are also expressed as pragmas: 43 Question: how are these expressed in the source code? 44 45 Answer: These are also expressed as pragmas: 44 46 {{{ 45 47 #pragma TASS jointinvariant skew(2:1) i == spec.j && k == spec.s + 1 … … 49 51 == Library calls == 50 52 51 Library calls will be modeled by creating abstract versions of the libraries. Syntactically, in the model these will also be function calls just like other function calls. 53 Question: real C programs make lots of calls to library functions. How are these modeled? 54 55 Answer: Library calls will be modeled by creating abstract versions of the libraries. Syntactically, in the model these will also be function calls just like other function calls. 52 56 There are three types of functions that can be called: 53 57 … … 64 68 65 69 == Example == 70 66 71 Here is a program that adds the elements in a file. The commandline argument is the filename. Inputs are the filename, the contents of the file, and the parameter B which is an upper bound on the number of elements that will be read. Output is to stdout. 67 72 68 How do we annotate this file in such a way that it does not interfere with compilation, but provides all the information we need to build a TASS model?73 Question: How do we annotate this file in such a way that it does not interfere with compilation, but provides all the information we need to build a TASS model? 69 74 75 Answer: proposed solution is embedded in the source below... 70 76 71 77 {{{ … … 119 125 == Pragmas == 120 126 121 Here is a list of pragma types we need: 127 Question: what are all the pragmas we will need, and what will be there exact syntax and semantics: 128 129 Answer: Here is a proposed list: 122 130 123 131 * {{{#pragma TASS assert <TASS expression>}}} 132 * verify that the expression is true; report an error if it is not 124 133 * {{{#pragma TASS assume <TASS expression>}}} 134 * assume the expression is true, i.e., add the value of this expression to the current path condition 125 135 * {{{#pragma TASS invariant <TASS expression>}}} 136 * this is an (ordinary) loop invariant. Check that it really is an invariant, and use that fact to compute the state after the loop exit 126 137 * {{{#pragma TASS jointinvariant <TASS expression>}}} 138 * this is a joint loop invariant relating this loop to a loop in the specification program. Use to check functional equivalence. 127 139 * {{{#pragma TASS ignore}}} 140 * ignore the next statement (typically used for I/O statements that are not relevant) 128 141 * {{{#pragma TASS input <type> <variable>}}} 142 * treat the next element as an input variable. Could be a preprocessor directory defining an object-type macro. 129 143 130 144 Grammar of TASS expressions:
