employeeConstants.lsl

employeeConstants.lsl

employeeConstants: trait
  assumes CTrait
  introduces
    maxEmployeeName, employeePrintSize: -> int
  asserts equations
    maxEmployeeName > 0 /\ maxEmployeeName <= 20;
    employeePrintSize > 0 /\ employeePrintSize <= 80

Return LCLint Home Page David Evans
University of Virginia, Computer Science
evans@cs.virginia.edu