I have a dockerized Deal that I can successfully run using docker run -it -v `pwd`:/scratch -w /scratch --rm deal python3 -m deal prove deal_demo_cat.py which produces deal_demo_cat.py cat ...

I am new to Design by contract methodology. I am writing a jml code using openjml to specify the contractes to the methods in a class. I have implemented a Subtraction class with the method subtract, ...

I want to be able to include information about my type in the Predicate_Failure message. Here's what I have that works: subtype Norm is Float range 0.0..1.0; type Component is (Red, Green, Blue, ...

I have a question related to applying contracts in a critical environment. Imagine I have the following function to divide: function div (dividend, divisor : Float) return Float with Pre => divisor ...

Here is my class: @Stateless @Transactional public class PostService { @Inject private PostRepository postRepo; @Inject private UserRepository userRepo; @Inject private SectionRepository ...

in last exam, I've had question, I was unable to answer sanely. Question was "what problems might arise from too weak precondition?" Another question was "what problems might arise from ...

I have been reading into the topic of Design By Contract and so far have the following notes written: When strengthening a condition, it means to make it more restrictive and weakening a condition is ...

I am studying the 'Design by Contract' development methodology. However, I am having a hard time seeing its advantages. For example, it is said that one of the characteristics of this methodology is ...

How do I raise an exception further in eiffel? I have 3 cases I want to retry a_feature local l_retries_count: INTEGER do some_potential_failing_feature rescue if ...

I was trying to have a structure which talks himself about variants and invariants into Eiffel loops, but don't understand the variant part! from l_array := <<1,2,30,60>> l_index :=...

Sometimes the checks and contract constructions need an elaboration which wants to be avoided when assertions removed to improve performances and avoid doing useless things with the "only" ...

Is there a way to specify a custom error/on failure message for pre- and postconditions, by analogy with Predicate_Failure for predicates? I can't seem to be able to find anything in the official ...

I have an Activity, a Presenter, and a Contract which both the Activity and the Presenter implement. The Activity will have some unique UI stuff, which must be called from within the Presenter. The ...

Eiffel Studio seems to pass through my requirements even if I have them enabled on project settings. And as far as I remember I was able some time to put a break point into the requirements... I don'...

I have a very simple express js server that accepts a request from a client, performs some business logic and respond back to the client. The request - response pipeline is handled by a controller and ...