| progr. |
partition (входных данных; list of conditions of inputs with their associated expected output, verifying the following criteria: 1) The full spectrum of all potential values is covered, 2) There is no overlap between partitions. These criteria can be verified either dynamically, by verifying at test time that all inputs exercised fall into one and only one partition, or formally proving that the partition are indeed complete and disjoint. An example of such partitioning with two input variables in Ada 2012: function ArcTan (X, Y : Float) return Float with Contract_Cases => (X >= 0 and Y >= 0 => ArcTan’Result >= 0 and ArcTan’Result <= PI / 2, X < 0 and Y >= 0 => ArcTan’Result >= PI / 2 and ArcTan’Result <= PI, X < 0 and Y < 0 => ArcTan’Result >= PI and ArcTan’Result <= 3 * PI / 2, X >= 0 and Y < 0 => ArcTan’Result >= 3 * PI / 2 and ArcTan’Result <= 2 * PI) Alex_Odeychuk) |
