CALL FOR PAPERS FOR THE
9th ICOOOLPS Workshop
Implementation, Compilation, Optimization of OO Languages,
Programs and Systems
July 28th 2014, Uppsala, Sweden
Colocated with ECOOP
- DEADLINE EXTENDED: 1 May 2014
Call for Contributions
WING 2014: 5th International Workshop on Invariant Generation
23 July 2014. Vienna, Austria
http://vsl2014.at/meetings/WING-index.html
** Important Dates: **
Submission deadline: 1 April 2014
Workshop: 23 July 2014
** About WING
Hi,
My function for finding the max number of a list is as follows:
val Max_List = Define ( Max_List []= NONE)
/\ ( Max_List (h::l) = let max= Max_List l in
( if h max then SOME h else if h = max then NONE
(else( Max_List l)))
I do not know whats wrong with this?
Can anybody help please?
Hi,
Problem is that the max computed on the tail of the list
let max = Max_List l
is an element of an option type, so has the form of NONE or SOME m.
However, you are directly comparing max with a number. So the type
system is angry at you!
Try this instead:
val Max_List =
Define
The code has a mistake which results in
!l. Max_List l = NONE
being provable which is probably undesirable. This can
be repaired by adding a clause
(Max_List [x] = SOME x)
to the definition/ Also, you might consider changing it to
use = rather than .
Konrad.
On Thu, Apr 24, 2014 at
