check_functions.tex 5.54 KB
 julien.delange committed Apr 14, 2010 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 \label{check_function} \paragraph{} \texttt{Verification functions} are functions which can be called within the \texttt{verification expression}. Their is two kinds of verification functions : \begin {itemize} \item \texttt{set-based functions}, which always takes a set or element as first parameter, and can have others parameters (usually literal). They always returns a value or a list of values. eg : Cardinal, Get\_Property\_Value, Property\_Exists; \item \texttt{value manipulation functions}, where the single parameter is a value or a list of values, and which returns another value. \end {itemize} \subsubsection {Property\_Exists} \textit {Property\_Exists} takes two parameters, an element or a set and a string literal. If the first argument is an element, then it returns true if the specified property is defined on this element, and else in the other case. If the first argument is a set, it returns true if all the the specified property is defined on all the elements of the set. The \textit{Exists} function is an alias of \textit {Property\_Exists}. \subsubsection {Get\_Property\_Value} \textit {Get\_Property\_Value} takes two parameters, an element or a set and a string literal. It returns the either the value of the property whose name is the second parameter in the node designed by the first parameter, if the first parameter is an element, or a a list of values which are the results of the application of \textit {Get\_Property\_Value} on each element of the set. The \textit {Property} function is an alias of the \textit {Get\_Property\_Value} function. This is currently the only way to produce a list of values. \subsubsection {Cardinal} \textit {Cardinal} takes a set as parameter. It returns the set cardinal (ie. an integer). \subsubsection {First} \textit{First} is a function which cann be applied on a range or on a list of range. It returns respectively a float element (even if the actual value of the AADL range term was an integer) or a list of floats, which are the lower bounds of each range of the list. Whenever called on a empty list, it returns another empty list. However, when called on a nil argument, it returns an error and the theorem is therefore considered false. \subsubsection {Last} \textit{Last} is a function which can be applied on a range or on a list of range. It returns respectively a float element (even if the actual value of the AADL range term was an integer) or a list of floats, which are the Upper bounds of each range of the list. Whenever called on a empty list, it returns another empty list. However, when called on a nil argument, it returns an error and the theorem is therefore considered false. \subsubsection {List} \textit{List} is a function which can be applied on a set of literals, or on a REAL \textit{Set}. In the first case, it build a list that contains the values given as paremeters. In the second case, it build a list of \textit{Elements} which are the set's elements. \subsubsection {Size} \textit{Size} is a function which can be applied on any kind of list. It returns the number of elements in the list (an integer value). \subsubsection {Head} \textit{Head} is a function which can be applied on any kind of list. It returns the first element of the list (ie. on a list of integers, it will return an interger). Whenever called on a empty list, it returns an error and the theorem is therefore considered false. Thus, test should be done using a ternary expression and the \textit{Size} function on the list. \subsubsection {Queue} \textit{Queue} is a function which can be applied on any kind of list. It returns the list without the first element. Whenever called on a empty list, it returns an error and the theorem is therefore considered false. Thus, test should be done using a ternary expression and the \textit{Size} function on the list. \subsubsection {Max} \textit {Max} is a function which can be applied on a list of floats or integers as parameter. It always return a float which is the highest value found. Note that the only way to produce the list is currently to call the Get\_Property\_Value on a list. \subsubsection {Min} \textit {Min} is a function which can be applied on a list of floats or integers as parameter. It always return a float which is the lowest value found. Note that the only way to produce the list is currently to call the Get\_Property\_Value on a list. \subsubsection {Sum} \textit {Sum} is a function which can be applied on a list of floats or integers as parameter. It always return a float which is the sum of all the values found. Note that the only way to produce the list is currently to call the Get\_Property\_Value on a list. \subsubsection {Product} \textit {Product} is a function which can be applied on a list of floats or integers as parameter. It always return a float which is the product of all the values found. Note that the only way to produce the list is currently to call the Get\_Property\_Value on a list. \subsubsection {GCD} \textit {GCD} is a function which can be applied on a list of floats or integers as parameter. It always return a float which is the Greatest Common Divisor of all the values found. Note that the only way to produce the list is currently to call the Get\_Property\_Value on a list. \subsubsection {LCM} \textit {LCM} is a function which can be applied on a list of floats or integers as parameter. It always return a float which is the Lowest Common Multiple of all the values found. Note that the only way to produce the list is currently to call the Get\_Property\_Value on a list.