The prometheus from ionuttamas

Prove purity of solution methods

Currently we take first reacheable hit => must take all

If we have:

METHOD 1:
if (from1.Age == 12 && to1.Age == 14)

METHOD 2:
if (from2.Age == 12 && to2.Age == 14)

we take: from2 ~ from1 and to2 ~ from1.
We should also check to2 ~ to1 and from2 ~ to1 => all possible combinations.

Reason about collections

Count, contains checks:

if (lv != null && lv.SelectedItems != null && lv.SelectedItems.Count > 0)
            {
                SelectedItems = lv.SelectedItems.Cast<ListViewItem>().Select(x => x.Tag as WorkerTask).Where(x => x != null && x.Info != null).
                    Select(x => new UploadInfoStatus(x.Info)).ToArray();
            }

Add tests for pure methods with different arguments

Implement conditions for return statements

  public static Customer GetFirstLinq(List<Customer> customers, Customer from, decimal amount)
    {
        if (from.AccountBalance > amount)
            return customers.First(x => x.Age > from.Age);

        if (from.Type == CustomerType.Gold)
            return from;

        return customers.First(x => x.DeliveryAddress == from.DeliveryAddress);
    }

the return customers.First(x => x.DeliveryAddress == from.DeliveryAddress); should have as conditions the negations of the 2 if statements.

3rd party assignments need to be tracked until initial assignment (currently we track the first assignment only)

Boolean functions in conditions

E.g. add support for

if ( IsValid(instance) )
 {
       ....
 }

or

if ( instance.IsValid() )
 {
       ....
 }

should elevate the IsValid return types as Z3 conditions.

Boolean properties handling in test conditions

Track polymorphic call sites for interfaces with multiple types

The developer can specify that a field can have multiple implemented types => the polymorphic service should support that.

Add asynchronous tasks support

Add support for out parameters

Track polymorphic call sites for interfaces

Track variables read from external sources

If we have:

customer.Age = valueFromFile(...);
then customer.Age can have any value.

If a check is made, such as:

var value = valueFromFile(...);

if (value>0)
{
   customer.Age = value;
}

Implement method tracker for method assignment

Add support for signals synchronization

Check also for constraints within the same expression

if ( a == 2 && c == 3)

=> check if a ~ c as well.

Property assignment tracking

Fix enums: "Enum.Value" appearing in 2 places should have the same value

Add Task support

When crossing variables in comparisons => check for distinct only

Implement boolean method Z3 model implementation

Add null support

Track polymorphic call sites for abstract methods

Test null/null checks for parameters

Handle boolean methods and methods included in boolean expressions in conditions

Implement constants handling

Test static 3rd party complex method reference assignments: member check

Implement extension methods assignment handling

Handle external and internal references

Handle:

bool flag;

if ( ... )
{
  flag = externalRef;
}
else
{
   flag = internalRef;
}

Handle non-boolean binary expressions in condition tests

Handle:

if ( a+b>c)

ionuttamas / prometheus Goto Github PK

prometheus's People

Contributors

Watchers

prometheus's Issues

Recommend Projects

Recommend Topics

Recommend Org