Sheaf tools for computation

The paper presents first how we can compute sheaf tools for accomplishing our goal, i.e. an authentication method by sheaves. We are using the most general notion of a sheaf, as a functor on a site, which is a category equipped with a Grothendieck topology. Moreover, we have introduced a notion in sheaf theory, family for matching, in order to simplify the sheaf definition in a computation class of sites called well structured sites. This has given us the possibility to construct an optimal validation algorithm of sheaves. Also, we present an algorithm to generate sheaves. By handling the concepts of Goguen, the behaviour of a system is computed in the internal language of a (pre)sheaf topos. Non-interference by Goguen is also computed in the internal language of a presheaf topos by using predicates.