Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
Other
712
stars
123
forks
source link
signature types for predicate and function arguments should always be checked #133
Invocations of functions and predicates are type-checked by ensuring that the actual argument
expressions are not disjoint from the formal arguments. Functions and predicates, like fields, may
be overloaded, so long as all usages can be unambiguously resolved by the type checker.
The constraints implicit in the declarations of arguments of functions and predicates are conjoined
to the body constraint when a function or predicate is run. When a function or predicate is
invoked (that is, used within another function or predicate but not run directly), however, these
implicit constraints are ignored. You should therefore not rely on such declaration constraints to
have a semantic effect; they are intended as redundant documentation. A future version of Alloy may
include a checking scheme that determines whether actual expressions have values compatible
with the declaration constraints of formals.
I think what this says is that if you have a model:
sig Base {}
sig S extends Base {}
pred finding[s : S] {
then finding will ensure that s is of type S when it's called directly from a run, but not when it's called from
another predicate or function. In which case you have to explicitly check s in S at the beginning of the implementation.
This is a usability accident waiting to happen. predicate/function argument types should be checked in every case.
zsfre
commented
4 years ago
From Sect. B.6.4 of the Green Book:
I think what this says is that if you have a model:
then
findingwill ensure thatsis of typeSwhen it's called directly from arun, but not when it's called from another predicate or function. In which case you have to explicitly checks in Sat the beginning of the implementation.This is a usability accident waiting to happen. predicate/function argument types should be checked in every case.