Steven D'Aprano writes: > Wasn't me, it was the other Stephen who spells his name with a "ph" > :-)
Guilty as charged, on both counts. > So each loop will need its own context manager, meaning its own > class. The *actual* invariant will be buried far away, in a CM > class, rather than right there next to the loop. I see no reason why that will be true for many invariants. The context manager class would be simple, in principle: __entry__, __exit__, and invariants. The expression in the with statement would be a constructor. > Worse: the condition will likely need to be written as a string, or a > lambda, in order to delay evaluation. Or a local def. This is correct, as far as I know. I would expect the example from Wikipedia (https://en.wikipedia.org/wiki/Loop_invariant#Informal_example) translated to Python would be written in the "condition as string" implementation as def max(n, a): m = a[0] # m equals the maximum value in a[0...0] i = 1 while (i != n) { with Invariants('m == max(a[0:i])'): # m equals the maximum value in a[0...i-1] if (m < a[i]): m = a[i] # m equals the maximum value in a[0...i] i += 1 # m equals the maximum value in a[0...i-1] # m equals the maximum value in a[0...i-1], and i==n return m So that's a little bit ugly because the condition is a string. The real problem I see is getting access to the bindings, which is likely to involve passing in globals() and locals() to the constructor, which isn't nice but also not so bad: Invariants(globals(), locals(), 'm = max(a[0:i])', # add more invariants here if you like ) Unfortunately, locals() is not guaranteed by the language to update with changes to the locals (although it appears to in CPython 3.8.2). > In Eiffel, invariants are a block. In Python, I suspect you would want each invariant to be a suite, since the calculations you can do with expressions are limited, and you wouldn't want to define a function for the reasons of locality to the loop that you mentioned already. > Forcing invariants into a context manager would have all the > disadvantages of forcing every for loop into a call to map() with a > named function. I really doubt it. I think some complex invariants would need to be implemented as named functions, but much of the time all of the invariants could be inlined, and almost all of the time most of the invariants could be inlined. > I don't think the context manager idea will be practical unless you > have only a very small number of very similar, simple, invariants. I agree, but I also think that generalizes to the whole idea of invariants in Python. I don't think programming with invariants is likely to be Python's strong suit. I'd loved to be proved wrong (not that I'd use them myself that I can see, but I know others have explored the idea of automatically verifying invariants and it would be cool!) If so, I'd be supportive of a syntax change. Steve _______________________________________________ Python-ideas mailing list -- python-ideas@python.org To unsubscribe send an email to python-ideas-le...@python.org https://mail.python.org/mailman3/lists/python-ideas.python.org/ Message archived at https://mail.python.org/archives/list/python-ideas@python.org/message/AZMTNAB4MTILJLSSNTROP3DLH5NVSG33/ Code of Conduct: http://python.org/psf/codeofconduct/
