Permalink
Commits on Sep 23, 2013
  1. Changing order of region names

    atzannes committed Sep 23, 2013
  2. Merge branch 'master' of github.com:dpj/DPJizer

    Conflicts:
    	prolog/example2.pl
    	prolog/example3.pl
    atzannes committed Sep 23, 2013
Commits on Jul 24, 2012
  1. Added dpj functionality

    * substitution on effects and on effect sets
    * nonInterference over a set of effect sets (removes the need to manually create,
      for each effect set, the union of the effect sets we want it not to interfere
      with).
    
    Added exampl3b which is identical to example3 but uses effect substitution
    instead of duplicate RPL substitution predicates.
    atzannes committed Jul 24, 2012
Commits on Jul 12, 2012
  1. Adding file with "unit tests" for dpj.pl

    Adding the 3 example files.
    atzannes committed Jul 12, 2012
Commits on Jul 11, 2012
Commits on Jul 3, 2012
  1. A couple of minor stylistic changes to the dpjizer.region.core and to…

    … the smt/dpjizer.smt2
    atzannes committed Jul 3, 2012
Commits on Aug 17, 2011
  1. Added isNested and expected output.

    The nesting relation is defined recursively in the formalism of the DPJ type system. But, we have defined this relation for RPL's of length up to two to avoid recursion in Z3.
    
    This commit belongs to issue #15.
    reprogrammer committed Aug 17, 2011
  2. Removed the list representation of RPLs.

    Remove the list representation to avoid the recursion in the definition of "append".
    
    This commit belongs to issue #15.
    reprogrammer committed Aug 17, 2011
  3. Made cons, makeRPLElement and makeRPL one-to-one functions.

    The function "append RPL RPLElement" makes the program nonterminating perhaps because it's interpreted as a recursive function.
    
    This commit belongs to issue #15.
    reprogrammer committed Aug 17, 2011
  4. Removed the recursive functions.

    Defines the "last" function without recursion.
    
    Checked the correctness of the function "disjointness" for disjointness from right.
    
    This commit belongs to issue #15.
    reprogrammer committed Aug 17, 2011
Commits on Aug 3, 2011
  1. Bounded the lenght of RPLs.

    Z3 does not terminate.
    
    This commit belongs to issue #15.
    reprogrammer committed Aug 3, 2011
Commits on Aug 1, 2011
  1. Added formulas for defining the "isFullySpecified" function.

    This commit belongs to issue #15.
    reprogrammer committed Aug 1, 2011
Commits on Jul 20, 2011
  1. Encoded a few rules of DPJ in SMT-Lib v2.

    This commit belongs to issue #15.
    reprogrammer committed Jul 20, 2011
Commits on Jul 12, 2011
  1. Made the String representations of disjointness and equality constrai…

    …nts shorter
    
    This commit belongs to issue #12.
    reprogrammer committed Jul 12, 2011
  2. Converted the constraints on the equality of complex RPLs into simple…

    …r ones.
    
    Translated the constraints on the equality of RPLs that have substitutions with equality constraints on RPLs without substitutions.
    
    This commit belongs to issue #12.
    reprogrammer committed Jul 12, 2011
Commits on Jul 8, 2011
  1. Processed the disjointness constraints by reasoning about the structu…

    …re of RPLs.
    
    This commit belongs to issue #12.
    reprogrammer committed Jul 8, 2011
  2. Made begins-with and contains constraints work on RPL arguments.

    Changed begins-with and contains constraints to take an RPL rather than RPLElement.
    
    This commit belong to DPJizer #12.
    reprogrammer committed Jul 8, 2011
Commits on Jun 29, 2011
  1. Implemented the solver for the collected constraints.

    This commit belongs to issue #12.
    reprogrammer committed Jun 29, 2011
Commits on Jun 28, 2011
  1. Replaced begin-with constraints containing substitutions by simpler c…

    …onstraints
    
    This commit belongs to issue #12.
    reprogrammer committed Jun 28, 2011
Commits on Jun 27, 2011
  1. Prepared for solving begin-with constraints.

    - Enabled ConstraintRepository.solve.
    - Added RPL.shouldContainOrBeginWithRPLElement(RPLElement, ConstraintKind)
    
    This commit belongs to issue #12.
    reprogrammer committed Jun 27, 2011
Commits on Jun 22, 2011
  1. Translated the region-inclusion constraints into begins-with constrai…

    …nts.
    
    This commit belongs to issue #12.
    reprogrammer committed Jun 22, 2011
Commits on Jun 15, 2011
  1. Generated read/write disjointness constraints.

    Generated read/write disjointness constraints from DPJ foreach loops. Then, generated begin-with constraints from the disjointness constraints and generated lower level begin-with constraints by propagating fresh region names along the substitution chain.
    
    This commit belong to issue #12.
    reprogrammer committed Jun 15, 2011
Commits on Jun 9, 2011
  1. Inserted the loop index variable into read effects of foreach loop if…

    … possible.
    
    This commit belongs to DPJizer issue #12.
    reprogrammer committed Jun 9, 2011
  2. Fixed an expected file of ReadWriteDisjointness.

    This commit belongs to issue #12.
    reprogrammer committed Jun 9, 2011
Commits on Jun 8, 2011
  1. Added simple test for recursion and disjointness of read/write effects.

    This commit belongs to issues #12, #13.
    reprogrammer committed Jun 8, 2011
Commits on Jun 7, 2011
  1. Introduced a read effect inside the foreach loop.

    Added a statement inside the foreach whose read effect cannot be made disjoint from the write effects by means of the loop index variable.
    
    This commit belongs to issue #12.
    reprogrammer committed Jun 7, 2011
Commits on Jun 2, 2011
  1. Stopped using [?] to distinguish write effects across loop iterations.

    The effects that contain the loop index variable of the foreach loop are disjoint. But, the effects that contain the RPL element [?] are not necessarily disjoint across different iterations of a foreach loop. Therefore, we changed the code so that it doesn't consider two effects containing [?] to be disjoint.
    
    This commit belongs to issue #11.
    reprogrammer committed Jun 2, 2011
  2. Generated constraints to make the write effects of foreach loops disj…

    …oint.
    
    This belongs to issues #9 and #11.
    reprogrammer committed Jun 2, 2011
Commits on May 18, 2011
  1. Generated the constraints to distinguish the write effects of foreach…

    … loops.
    
    This commit belongs to issue #11.
    reprogrammer committed May 18, 2011
Commits on May 3, 2011
Commits on Mar 15, 2011
  1. Automatically tested the correctness of the generated constraints.

    Added the files containing the expected list of constraints for each test. Added automated checks to compare the actual list of generated constraints against the expected one.
    
    This commit belongs to issue #8.
    reprogrammer committed Mar 15, 2011
  2. Added the RPL inclusion constraints to a ConstraintRepository data st…

    …ructure.
    
    This commit belongs to issue #8.
    reprogrammer committed Mar 15, 2011