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

semantics of basic specs in CASL



A comment to the basic concepts of CASL: 

According to section 1.3, equations are of the form t_s = t'_s' 
and definedness formulas of the form D(t_s), where t_s and t_s'
are *sorted* terms (in ESTerm) and not just fully-qualified terms (in FQTerm).
I do not see any reason for explicitly sorting the terms, as the sort
of a term can always be derived (cf. the function "sort").

[I really don't understand why explicit sorts are required either, and
there is a comment at the end of section 2.3.3 to that effect.  They
are in the semantics only because they are mentioned in the text.  -- DTS]

Best regards,
  Anne 
------------------------------------------------------------------------------

Anne Elisabeth Haxthausen
Department of Information Technology	E-mail:	   ah@it.dtu.dk
Building 344       		        Phone:	   +45 45 25 37 50
Technical University of Denmark		Fax:	   +45 45 93 00 74   
2800 Lyngby			         
DK - Denmark				

------------------------------------------------------------------------------