A postcondition is some condition which must be satisfied after running a given section of code. It may be specified in code via assertions, or in the documentation.
Questions tagged [post-conditions]
58 questions
10
votes
5 answers
Can't weakening preconditions and strengthening postconditions also violate Liskov Substitution Principle?
Actual precondition of a subtype is created by combining ( using logical OR ) preconditions of a base type and preconditions of a subtype, which makes the resulting precondition less restrictive
Actual postcondition of a subtype is created by…
EdvRusj
- 745
- 7
- 14
6
votes
3 answers
What are preconditions and postconditions?
I'm learning how to program but one thing I can't quite get my head around is preconditions and postconditions.
Is an if statement before calling a function considered a precondition, or is there a separate more efficient way of doing this in most…
Simon J
- 71
- 1
- 1
- 2
5
votes
3 answers
Design by contract and assert statements
I am interested in the Design by Contract approach. It seems that for preconditions checked exceptions must be used to enforce them.
But for post-conditions and class-invariants I think that assertions are preferred.
Am I right? If I am correct, why…
Cratylus
- 52,998
- 69
- 209
- 339
4
votes
3 answers
Pre and Post Condition from Stroustrup's book
In chapter 5.10.1 of Programming: Principles and Practice using C++, there is a "Try this" exercise for debugging for bad input of an area. The pre-conditions are if the the inputs for length and width are 0 or negative while the post-condition is…
mcbalsa
- 51
- 5
4
votes
1 answer
How can class invariant strengthen pre and post-conditions?
Link
You can think of the class invariant as a health criterion, which must
be fulfilled by all objects in between operations. As a precondition
of every public operation of the class, it can therefore be assumed
that the class invariant…
EdvRusj
- 745
- 7
- 14
3
votes
1 answer
Clojure post-condition fails to execute due to syntax error -- why?
In this function:
(defn my-post
[a]
{:post (number? %)}
a)
The post-condition doesn't execute (or at least, doesn't cause an assertion error). I now know that it should have been:
(defn my-post
[a]
{:post [(number? %)]} ;; note the…
Matt Fenwick
- 48,199
- 22
- 128
- 192
3
votes
2 answers
Precondition and postcondition checks in public methods
I was reading the Oracle documentation about using the assert keyword to verify method preconditions and postconditions.
The document says that it's fine to use the assert keyword to verify postconditions for public methods but you should only use…
Ogen
- 6,499
- 7
- 58
- 124
3
votes
0 answers
Code contracts can't prove that elment exists in list
Basically, I want an element added to the list if it does not already exist in it. It seems reasonable to have a post-condition that ensures that this element exists in the list after method is done. Below is minimal example which gives me error…
user1242967
- 1,220
- 3
- 18
- 30
3
votes
5 answers
Java: weak pre condition and strong post condition, how to?
I'm having a really hard time in understanding how pre-conditions and post-conditions must work, without violate the Substitution Principle. So let's assume that we have a class Rectangle and Square—how to relate them? Which one must be the…
Francesco
- 521
- 1
- 6
- 14
3
votes
2 answers
What is a post-condition exception?
I'm doing some homework which has the question:
How would you a pre-condition exception?
How would you use a post-condition exception?
So for the first question, I assume a precondition is something that must be met in order for the function to run.…
Brugsen
- 603
- 1
- 6
- 12
3
votes
1 answer
Should client check postcondition/should called method check precondition?
The preconditions and the postconditions of the public method form a contract between this method and its client.
1.According to, caller shouldn't verify postcondition and called method shouldn't verify preconditions:
Let us recall the precondition…
EdvRusj
- 745
- 7
- 14
3
votes
1 answer
Loop invariant proof
I am running into an issue coming up with the post-condition and showing partial correctness of this piece of code.
{ m = A ≥ 0 }
x:=0; odd:=1; sum:=1;
while sum<=m do
x:=x+1; odd:=odd+2; sum:=sum+odd
end while
{ Postcondition }
I'm not…
Ross Verry
- 115
- 8
3
votes
1 answer
JML postcondition contains class method call
Can a JML postcondition for a class method contain a call to another method call
For example I have this class:
public class A
{
public int doA(x)
{ ... }
public int doB(int x, int y)
{ ... }
}
For the postcondition of doB can I…
Alina Danila
- 1,683
- 1
- 24
- 60
3
votes
1 answer
Proving correctness in formal logic
I was wondering if anyone could help me answer this question. It is from a previous exam paper and I could do with knowing the answer ready for this years exam.
This question seems so simple that I am getting completely lost, what exactly is it…
Paul Blundell
- 1,857
- 4
- 22
- 27
2
votes
1 answer
Equivalence of if-then and implies in OCL statements
Are the following two OCL statements equivalent for some function context?
post: if a > 0 then b < c
post: b < c implies a > 0
a_fan
- 383
- 2
- 22