[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.