CODEWITHSUNDEEP
pythonsemanticsformal-verificationpreconditionsformal-methods
desert_ranger
desert_ranger

Reputation: 1737

How to compute weakest preconditions for class methods with object state in Python?

I am working on a tool to compute weakest preconditions for certain Python programs, and I’m struggling with handling class objects and their variables. Here's a minimal example of the problem:

For a standalone function like this:

def square_number(n):
    return n * n

Computing the weakest precondition is straightforward. I can define a postcondition (e.g., result == 25) and then backtrack to derive the precondition (e.g., n == 5 or n == -5).

However, I’m unsure how to proceed when dealing with instance variables. For example:

class NumberSquarer:
    def __init__(self, k):
        self.k = k

    def square_number(self):
        return self.k * self.k

# Example usage
squarer = NumberSquarer(5)
result = squarer.square_number()  # Returns 25

In this case:

The square_number method depends on the instance variable self.k. The postcondition could be something like result == 25. My question is: How do I compute the weakest precondition for the method square_number given a postcondition, especially when the state is encapsulated in the object (e.g., self.k)?

If the method involves multiple instance variables or interactions between methods, how should I approach deriving the precondition systematically? Are there any tools or strategies (e.g., symbolic computation with libraries like SymPy) that can help?

Based on the comments and this book, this is how I derive the weakest preconditions for functions

Let square_number(n)<25,

then n^2<25

then the precondition would be n<5 or n>-5

I have no idea how to derive preconditions in the cases of classes and class variables. Please let me know if you have more questions.

Upvotes: 0

Views: 45

Answers (0)

Related Questions