Perhaps you agree with Lamport even harder than Lamport does. If your team is going to get together and implement "Set x to the smallest number >= to all eleme

Perhaps you agree with Lamport even harder than Lamport does. If your team is going to get together and implement "Set x to the smallest number >= to all elements of A", and you feel that that it's an ambiguous or incomplete description, then it's up to you guys to formalise what is meant - a programming activity - rather than just coding it. If it is as poorly-specified as you suggest, then someone on your team will think that they have correctly implemented it (tests and all!) but it will give the wrong answer in production.