[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] pvs, temporal logic and stacks

they have what they call model variables or ghost variables and the formula


An attempt at using model-based specification while at the same time being
independant of the implementation. Thus it has the easiness of model-based
specification and the generality of algebraic specification.