Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Support for inductively verifying contracts of recursive functions #2809

Merged
merged 24 commits into from
Oct 17, 2023
Merged

Support for inductively verifying contracts of recursive functions #2809

merged 24 commits into from
Oct 17, 2023

Commits on Oct 5, 2023

  1. Contract support for inductive verification of recursion

    @JustusAdam
    JustusAdam committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    291e6d0 View commit details
    Browse the repository at this point in the history

  2. Fix test cases, formatting

    @JustusAdam
    JustusAdam committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    18d7271 View commit details
    Browse the repository at this point in the history

  3. Update Documentation

    @JustusAdam
    JustusAdam committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    6ea4a1b View commit details
    Browse the repository at this point in the history

  4. Formatting test cases

    @JustusAdam
    JustusAdam committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    92c595a View commit details
    Browse the repository at this point in the history

  5. More whitespace

    @JustusAdam
    JustusAdam committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    481e7b5 View commit details
    Browse the repository at this point in the history

  6. This whitespace stuff is getting ridiculous

    @JustusAdam
    JustusAdam committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    ad7c2de View commit details
    Browse the repository at this point in the history

  7. AAttach require any

    @JustusAdam
    JustusAdam committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    65a2a17 View commit details
    Browse the repository at this point in the history

Commits on Oct 8, 2023

  1. Merge branch 'main' into inductive-recursion-for-function-contracts

    @JustusAdam
    JustusAdam committed Oct 8, 2023
    Configuration menu
    Copy the full SHA
    e20eccf View commit details
    Browse the repository at this point in the history

  2. Fix names in test cases

    @JustusAdam
    JustusAdam committed Oct 8, 2023
    Configuration menu
    Copy the full SHA
    a31176c View commit details
    Browse the repository at this point in the history

Commits on Oct 10, 2023

  1. Apply suggestions from code review 

    Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
    @JustusAdam @zhassan-aws
    JustusAdam and zhassan-aws committed Oct 10, 2023
    Configuration menu
    Copy the full SHA
    ba9ea4e View commit details
    Browse the repository at this point in the history

  2. Suggestions from Zyad

    @JustusAdam
    JustusAdam committed Oct 10, 2023
    Configuration menu
    Copy the full SHA
    6902193 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'main' into inductive-recursion-for-function-contracts

    @JustusAdam
    JustusAdam committed Oct 10, 2023
    Configuration menu
    Copy the full SHA
    0817544 View commit details
    Browse the repository at this point in the history

Commits on Oct 11, 2023

  1. Better self detector

    @JustusAdam
    JustusAdam committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    832f92c View commit details
    Browse the repository at this point in the history

  2. Unused name

    @JustusAdam
    JustusAdam committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    081f7d6 View commit details
    Browse the repository at this point in the history

  3. Fix import error, add fail on two test case

    @JustusAdam
    JustusAdam committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    5ebfac5 View commit details
    Browse the repository at this point in the history

  4. fmt

    @JustusAdam
    JustusAdam committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    67795ba View commit details
    Browse the repository at this point in the history

  5. Added test case for, and fixed self detector

    @JustusAdam
    JustusAdam committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    6c58d37 View commit details
    Browse the repository at this point in the history

  6. Actually run the new test in regression

    @JustusAdam
    JustusAdam committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    8ad2ae0 View commit details
    Browse the repository at this point in the history

  7. Expand test case to also fail on postcondition

    @JustusAdam
    JustusAdam committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    9cd5ed1 View commit details
    Browse the repository at this point in the history

  8. Explanation for test case

    @JustusAdam
    JustusAdam committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    dd45198 View commit details
    Browse the repository at this point in the history

  9. fmt

    @JustusAdam
    JustusAdam committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    d2e3379 View commit details
    Browse the repository at this point in the history

Commits on Oct 17, 2023

  1. A few missing bits of documentation.

    @JustusAdam
    JustusAdam committed Oct 17, 2023
    Configuration menu
    Copy the full SHA
    281e6c1 View commit details
    Browse the repository at this point in the history

  2. Apply suggestions from code review 

    Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
    @JustusAdam @zhassan-aws
    JustusAdam and zhassan-aws committed Oct 17, 2023
    Configuration menu
    Copy the full SHA
    e651f6e View commit details
    Browse the repository at this point in the history

  3. Merge branch 'main' into inductive-recursion-for-function-contracts

    @JustusAdam
    JustusAdam committed Oct 17, 2023
    Configuration menu
    Copy the full SHA
    3623c16 View commit details
    Browse the repository at this point in the history