Project

General

Profile

Edit History

База данных ограничений » History » Version 3

Andrei Tatarnikov, 12/21/2011 12:16 PM

1 3 Andrei Tatarnikov 
h1. Constraint Solver
2 1 Alexander Kamkin 





    3
    3
    Andrei Tatarnikov
    
The constraint solver subsystem is aimed to provide a possibility to automatically generate test cases based on specified constraints. A constraint is represented by a set of limitations for input values. The solver suggest values of input variables which will violate the limitations. The solver implementation is based on 





    4
    1
    Alexander Kamkin
    





    5
    3
    Andrei Tatarnikov
    
In the current version, we use the Z3 solver by Microsoft Research.





    6
    
    
    





    7
    
    
    
It is based on 





    8
    
    
    





    9
    
    
    





    10
    
    
    





    11
    1
    Alexander Kamkin
    
h1. Constraint Solver Library





    12
    3
    Andrei Tatarnikov
    





    13
    
    
    
The ru.ispras.microtesk.constraints package includes the following sub-packages:





    14
    
    
    





    15
    
    
    





    16
    
    
    





    17
    
    
    
h2. Language-independent syntax tree





    18
    
    
    





    19
    
    
    





    20
    
    
    





    21
    
    
    





    22
    
    
    
h1. База данных ограничений





    23
    
    
    





    24
    
    
    
База данных ограничений строится автоматически в результате анализа формализованных спецификаций системы команд микропроцессора, выполненной на одном из ADL-языков (например, nML). Некоторые ситуации могут описываться вручную и добавляться в базу данных ограничений.